Table of content

Stream: Lean for teaching

[Sina]

On a Markdown file, in VScode i can generate a hyperlinked table of content at the top of the file. Is there such a functionality for Lean files?

[Chris Lovett]

This Natural Numbers Tutorial (derived from the famous Natural Number Game) is written in Lean then uses LeanInk to create markdown then it uses mdbook to generate nice HTML with a TOC on the left, the TOC comes from SUMMARY.md. The result looks like this https://lovettsoftware.com/NaturalNumbers/