what's the difference between coq and literate coq?
where did you get "literate Coq" from? Usually, it just refers to "literate programming" by Knuth applied to Coq, as in, e.g., Alectryon, see the Alectryon paper
software foundations "available as literate coq files", also it's all over the place in
I recently wrote about this distinction of books (literate vs. non-literate) in this preprint, see page 10, I call them "executable textbooks" vs. "traditional textbooks [with Coq libraries]"
i like executable textbooks
what the Software Foundations authors mean at a low level with "literate Coq files" is that their book content is written as special comments in Coq code, and then the
coqdoc tool and/or jsCoq generates HTML that interleaves code/prose which is how people usually consume the book (through their browsers).
Quinn has marked this topic as resolved.
Last updated: Oct 03 2023 at 21:01 UTC