Zulip Chat Archive

Stream: general

Topic: Presenting Lean code in LaTeX


view this post on Zulip James Palmer (Aug 19 2020 at 13:48):

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 :)

view this post on Zulip Alex J. Best (Aug 19 2020 at 13:50):

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

view this post on Zulip James Palmer (Aug 19 2020 at 14:07):

thank you very much!

view this post on Zulip James Palmer (Aug 19 2020 at 16:29):

@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?

view this post on Zulip Alex J. Best (Aug 19 2020 at 16:31):

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

view this post on Zulip James Palmer (Aug 19 2020 at 16:32):

Thank you very much!

view this post on Zulip Alex J. Best (Aug 19 2020 at 16:35):

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

view this post on Zulip Alex J. Best (Aug 19 2020 at 16:35):

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

view this post on Zulip James Palmer (Aug 19 2020 at 16:37):

amazing, thank you very much!


Last updated: May 15 2021 at 23:13 UTC