Topic: Lean in Latex
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!
Johan Commelin (Jun 01 2020 at 11:17):
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
Shenyang Wu (Jun 01 2020 at 11:30):
@Markus Himmel Got it. I'll try this. Thank you very much!
Ryan Lahfa (Jun 01 2020 at 15:31):
I use minted
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