The tool is all implemented in OCaml. The monadic-design pattern of parsing JSON comes from what I learned in Faial <https://gitlab.com/umb-svl/faial/> and I think it looks neat.

The output is Markdown-formatted and the tool can figure out your Rocq project. I've been using this to help Claude Code help me, with some success. I have some scratch files in the project, including playing around with Fleche, but I haven't figured that code base yet.

I'm learning to use Claude code for my Rocq proof development. First rule of fight club: If ANY proof attempt fails to compile, STOP IMMEDIATELY.

Otherwise, Claude just exhausts my tokens.

Original post: types.pl/@liamoc/1145...

Here's a short demo I gave to my students on proving a simple result without ltac (functional style). #Rocq

gist.github.com/cogumbreiro/...

@ NEPLS

I bought @unpackinggame.com. The objective is to organize a room that you just moved in. You're unpacking these boxes and placing the items in drawers, closets etc.

I love the irony of playing Unpacking while being at a messy room that I should be cleaning. It's a unique game in that way.

I got it to work! I had to prove equality "axiomatically", but it worked out.

gist.github.com/cogumbreiro/...

I tried this, but not getting much farther.

That being said, this is my first time playing with GADTs, so I'm just mashing keys.

3 of my favorite home-brewed tactics are
- invc H (which does `inversion H; subst; clear H`)
- `rename_hyp PATT as H`, which renames an assumption given a pattern PATT with name H
- `invc_hyp PATT`, which performs `invc` on an assumption given by a pattern PATT. #RocqLang #CoqLang

Early steps on verifying time for imperative programs.

Oh, I just tried the reverse exercise and it also did pretty well! The future is now. I'm loving the idea of generating latex from this.