minutes with Lean 3

Stream: general

[Jireh Loreaux]

In TPIL4 there is a note about how to use minted with Lean 4, and there is a corresponding lean4.py script. Question: where is the analogous information and script for Lean 3?

[Kevin Buzzard]

This information definitely exists on the discord (because students write projects) but IIRC it's of the form "minted just works out of the box"

[Eric Wieser]

The corresponding lean3.py is the theorem.py that ships as part of Pygments. minted does indeed work out of the box if your box has a recent enough version of Pygments installed.

[Jireh Loreaux]

Thanks both.