## Stream: maths

### 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!

(deleted)

#### 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!

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