Lean 4 (Meta)programming Cookbook

Indexing🔗

To add a term to the index, use the {index} role. This will not render anything in the text but will add the entry to the generated index, like: {index}[Term to index]