Lean in Latex

Stream: maths

[Shenyang Wu]

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]

(deleted)

[Markus Himmel]

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

[Shenyang Wu]

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

[Ryan Lahfa]

I use minted

[Ryan Lahfa]

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