Interactive Symbols🔗

To provide interactive features like hovers and type information for Lean symbols in your text, use the {name} and {lean} roles instead of plain backticks.

• {lean} `term`: Elaborates a full Lean expression (like {lean}`1 + 2`). It provides interactive info for every token in the expression.

• {name} `ConstName`: Resolves a global constant (like {name}`Nat`). It shows the docstring and type signature on hover.

Syntax:

The type {name}`Nat` is used for numbers. An example term is {lean}`[1, 2].map (· + 1)`.

Effect:

When rendered, hovering over Nat will show its definition and docstring. Hovering over parts of [1, 2].map (· + 1) will show types for the list, the map function, and the lambda abstraction.