Lean to Latex

Stream: new members

[Gabriel Moise]

Hello!
I wanted to write a project that has some Lean code attached to it in LaTeX, however I encountered some difficulties:

• there is no Lean option in the lstlisting environment, which means I can't get the pretty colouring etc. that I have for example in VS code
• in Lean there are a lot of symbols used, and it seems a little tedious to have to rewrite each of them to the LaTeX version of them for each line of code

Are there people who wrote Lean code into LaTeX who have any suggestions or sample LaTeX code?

[Eric Wieser]

Somewhere on github there's a listings config file to solve these problems

[Eric Wieser]

I had a good experience with minted instead of listings, but it requires a recent version of the Python pygments package

[Eric Wieser]

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

[Holly Liu]

i followed the setup instructions and am confused on how to get the symbols to show up in LaTeX? i'm doing \lstinline{list \upalpha} which shows up as list \upalpha when compiled.

[Anne Baanen]

In a listing, you should write the actual Lean code, including Unicode characters. So something like \lstinline{list α} would work.

[Holly Liu]

is there an easier way to do this instead of copy and pasting each symbol?

[Anne Baanen]

I have my Linux system set up with a Compose key. So α is compose-*-a, β is compose-*-b, → is compose--->, ...

[Anne Baanen]

Or you can look into X Input Methods in general, I think there are a few that allow you to type LaTeX symbol names and get unicode characters

[Holly Liu]

thanks. i'll look into it

[Eric Rodriguez]

if you're on Windows, I strongly recommend WinCompose :)