latex

Stream: general

[Dean Young]

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]

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

[Mauricio Collares]

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

[Eric Wieser]

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