Zulip Chat Archive

Stream: general

Topic: org-mode

Simon Hudon (Mar 12 2018 at 19:59):

Has anyone ever used org-mode to do literate programming in Lean?

Andrew Ashworth (Mar 12 2018 at 21:03):

That's how Jeremy used to write TPIL

Andrew Ashworth (Mar 12 2018 at 21:04):

see https://github.com/leanprover/mkleanbook

Simon Hudon (Mar 12 2018 at 21:05):

Nice! thanks!

Last updated: May 02 2025 at 03:31 UTC