Blueprint Lean Code Link Preview Wiring

 Blueprint Lean Code Link Preview Wiring🔗

Compiled2026-07-01T21:39:45ZProject5f17f8aMerge pull request #222 from leanprover/chore/reference-blueprints-catalog-all-v4.30.0-v4.31.0Leanleanprover/lean4:v4.31.0VersoBlueprint5f17f8a
Definition17
uses 0used by 0✓L∃∀N

Statement with an associated Lean declaration link in the summary.

Lean code for Definition17●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.

Contents

  1. Blueprint Summary