1.1. A first example🔗

You can write prose alongside Lean code blocks, and Verso will elaborate the Lean in the same environment as the textbook so cross-references work seamlessly. Use Nat to inline-render a term, or Nat.succ to link to a declaration in the imported Lean environment.