4. Authored labels with punctuation
Imported papers often carry labels such as Chapter4:Theorem4.2.1 or
ImportedPaper:Theorem2.2. The canonical Lean Name is useful internally, but
the manifest also preserves the raw authored label for user interfaces.
Theorem4.1
Rendered from external Markdown source (statement): source/pages/page-13.md:1:0-8:0; no native Verso body is available.
Theorem 2.2
This second bodyless node uses a punctuation-heavy authored label. The manifest keeps the raw label and the external Markdown source separately from the Lean name used for generated declaration previews.
Lean code for Theorem4.1●1 definition
Associated Lean declarations
-
Nat.add[complete]
Associated Lean declarations
-
Nat.add[complete]
-
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.