Lean 4 (Meta)programming Cookbook

Tagging🔗

Inside each header/subheader you can define a tag like this-

%%%
tag := "my-tag"
number := false
%%%

This way, you can refer to this section later using the tag.

How to get the link to the tag? - You can find the tag in the URL when you navigate to that section on the website after clicking on the header.