Interesting, I was recently looking into doing this after seeing a similar request on discourse (not that I am a coq expert by any means). https://github.com/p

Interesting, I was recently looking into doing this after seeing a similar request on discourse (not that I am a coq expert by any means). https://github.com/philzook58/learnxinyminutes-docs/blob/master/learncoq.v https://github.com/philzook58/learnxinyminutes-docs/blob/mas... I was thinking about basically taking the OCaml one and transcribing it, leaving proving to a short blurb at the end and the references. Still useful I think.