lean slide in Typst

Stream: general

[Asei Inoue]

I want to create slides that include Lean code using Typst, but what would be the best way to do it?
Since this is my first time, I don’t really know how.
I’d like to hear from people who have already done the same thing.

[pandaman]

Typst provides basic code highlighting for Lean code by default.

Example: https://github.com/pandaman64/kansuugatamatsuri-2025/blob/ded41a48e0e2701c344f5373dc12cdf6454c22d8/main.typ#L80
image.png

[Michael Rothgang]

@Patrick Massot also used typst for slides, including Lean code.

[Eric Wieser]

What highlighter does typst use?

[Joscha Mennicken]

It uses https://github.com/trishume/syntect (which uses sublime text syntax files) with language definitions from https://github.com/CosmicHorrorDev/two-face

[Eric Wieser]

I assume it's using the syntax file from vscode then?

[Joscha Mennicken]

Yes (indirectly through the bat repo). bat already uses the syntax from the lean4 vscode extension but two-face seems to still use an old, lean3 version. Assuming two-face is somewhat maintained, typst should switch to lean4 after enough time passes.

[Joscha Mennicken]

two-face uses a manual process to follow the bat repo, and it was last updated via PR 3 months ago. At some point since then, bat switched form lean3 to lean4.

[Patrick Massot]

You can tell typst to use a more recent file, as documented in https://typst.app/docs/reference/text/raw/#parameters-syntaxes

[Patrick Massot]

You can use the syntax file from https://github.com/sharkdp/bat/pull/3322/