Zulip Chat Archive

Stream: maths

Topic: Lean in Latex


view this post on Zulip Shenyang Wu (Jun 01 2020 at 11:13):

Hi! Does anyone know how to type Lean code in Latex in a nice way? I am writing a report and want it to look nice. Thanks!

view this post on Zulip Johan Commelin (Jun 01 2020 at 11:17):

(deleted)

view this post on Zulip Markus Himmel (Jun 01 2020 at 11:25):

There is a Lean stylesheet for the listings package at https://github.com/leanprover-community/lean/tree/master/extras/latex

view this post on Zulip Shenyang Wu (Jun 01 2020 at 11:30):

@Markus Himmel Got it. I'll try this. Thank you very much!

view this post on Zulip Ryan Lahfa (Jun 01 2020 at 15:31):

I use minted

view this post on Zulip Ryan Lahfa (Jun 01 2020 at 15:32):

Here are some examples but I'm not happy enough with the results: https://github.com/RaitoBezarius/projet-maths-lean/blob/master/docs/chapitres/fpropworld.tex#L38
It gives rise to somewhat acceptable results sometimes, but it's fragile


Last updated: May 06 2021 at 17:38 UTC