2. Bodyless Markdown statement with Lean declarations
This theorem is not native Verso yet. The theorem directive intentionally has no body, but it still has source provenance, imported Markdown, and Lean declarations. The preview manifest must therefore keep the source and Lean data on the external-markup entry.
Theorem2.1
uses 0
markupMD✓L∃∀N
Used by 2
Rendered from external Markdown source (statement): source/pages/page-12.md:4:0-15:0; no native Verso body is available.
Theorem 2.1
For every natural number $n$, the imported source states that addition and multiplication have canonical recursive behavior.
- Source text is Markdown, not Verso.
- The Blueprint node is intentionally bodyless.
- Lean declarations are still attached to the manifest entry.
Lean code for Theorem2.1●2 definitions
-
defdefined in Init/Prelude.leancomplete
def Nat.add : Nat → Nat → Nat
def Nat.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.
-
defdefined in Init/Prelude.leancomplete
def Nat.mul : Nat → Nat → Nat
def Nat.mul : Nat → Nat → Nat
Multiplication of natural numbers, usually accessed 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.