A detailed information on formatting on Verso is explained at Verso Markup page. Read below for a consise summary of some of the most commonly used formatting options.
You can include Lean code that is elaborated directly within the document. This is useful for small snippets. Please note that your lean code should follow the Lean syntax conventions of naming, casing variables, etc.
def helloCookbook := "Welcome!"
#eval helloCookbook
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.
Verso provides a way to include docstrings for Lean definitions directly in the documentation. This is done using the {docstring} role(see more information here.
{docstring Nat.add}
which will look like this:
Nat.add : Nat → Nat → NatNat.add : Nat → Nat → Nat
Addition of natural numbers, typically used via the + operator.
This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.
If your code snippet will throw errors, you can indicate that using the usual #guard_msgs just above your code. The below example is taken from Displaying in the Infoview recipe.
def errorMessage' (msg : String) : CoreM Unit := do
Lean.logError m!"Error: {msg}"
/-- error: Error: something went wrong -/
#guard_msgs in
#eval errorMessage' "something went wrong"
This will look like this:
def errorMessage' (msg : String) : CoreM Unit := do
Lean.logError m!"Error: {msg}"
/-- error: Error: something went wrong -/
#guard_msgs in
#eval errorMessage' "something went wrong"
You can link to other sections using their tags like: {ref "tag-name"}[link text].
An example would be {ref "building-recipe"}[Back to top]. This would give effect as: Back to top.
You can add marginal notes that appear in the side margin like: {margin}[Marginal text]. This would give effect as: Marginal notes are great for extra context.
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]