Zulip Chat Archive

Stream: general

Topic: minted with Lean 3

Eric Wieser (Nov 17 2022 at 14:22):

Though if you have an old version of pygments, or want to customize it, you can just put a copy of theorem.py in your latex directory and pass some extra flags to minted in the same way as presumably the Lean 4 instructions do

Last updated: Dec 20 2023 at 11:08 UTC