7. Native rewrite after review
After review, an imported item can be rewritten as normal Blueprint prose while keeping the original source witness attached for auditability.
Theorem7.1
The reviewed theorem is now expressed directly in Verso. Its Markdown badge shows that the imported source is still connected to the node for comparison and future audits.
Lean code for Theorem7.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.