Zulip Chat Archive

Stream: Lean for teaching

Topic: Table of content

Sina (Jul 26 2022 at 17:19):

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 (Oct 14 2022 at 18:16):

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/

Last updated: Dec 20 2023 at 11:08 UTC