External Markup Source Showcase

1. Native Blueprint text with imported witnesses🔗

This first node has a normal Verso body. The source witnesses are review data: the header advertises that Markdown and TeX are attached, while the body remains the curated Blueprint text.

Definition1.1
uses 0used by 0markupMDmarkupTeX✓L∃∀N
Tagsexternal-sourcemixed-markupnative-body

A native Verso Blueprint node can carry external Markdown and TeX witnesses. The source markup remains available to the manifest and preview cache, but it does not replace the authored Blueprint body.

Lean code for Definition1.1●1 definition
  • defdefined in Init/Prelude.lean
    complete
    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.