search

leanprover-community / lean4-samples

Code samples for Lean 4
Apache License 2.0
69 stars 23 forks source link

Question: How do you run lean4 on mdbook? #24

Closed Seasawher closed 1 year ago

Seasawher commented 1 year ago

If you mouse over the lean code in the mdbook of Natural Number Game, you can see the type. How is this implemented?

If nothing is configured, the mdbook playground will only be able to execute rust code.