Zulip Chat Archive

Stream: general

Topic: latex


Dean Young (Sep 22 2022 at 18:22):

Beginner's question:

What are the options for latex support in a Lean programming environment?

I want to be able to produce a pdf or Lean output from the same code.

Adam Topaz (Sep 22 2022 at 18:47):

https://github.com/leanprover-community/lean/blob/master/extras/latex/lstlean.md

Mauricio Collares (Sep 22 2022 at 18:51):

And you can probably use pandoc to convert Lean/Markdown files to PDF

Eric Wieser (Sep 22 2022 at 19:09):

The other option not mentioned there is to use minted, which knows about Lean out of the box. Unicode can still be a struggle if you're not using XeTeX/LuaLaTeX


Last updated: Dec 20 2023 at 11:08 UTC