Presenting Lean code in LaTeX

Stream: general

[James Palmer]

Hi everyone, I appreciate this question probably gets asked all the time - but what is the best way to present Lean code in LaTeX?

Many thanks :)

[Alex J. Best]

There is a style file and some instructions at https://github.com/leanprover-community/lean/tree/master/extras/latex

[James Palmer]

thank you very much!

[James Palmer]

@Alex J. Best does this work with Overleaf or do I need to actually download LaTeX Editor & the github code onto my laptop to use it?

[Alex J. Best]

I think it should work on overleaf, just upload the file lstlean.tex to your overleaf project as a separate file? I'll try it quick and let you know

[James Palmer]

Thank you very much!

[Alex J. Best]

Yeah it works for me, I clicked the upload button in the left file menu, then upload from external url and pasted https://raw.githubusercontent.com/leanprover-community/lean/master/extras/latex/lstlean.tex in

[Alex J. Best]

Then I copied the sample article tex to the article and it compiled fine!

[James Palmer]

amazing, thank you very much!