External Summary Links

 External Summary Links🔗

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

External declaration wiring test.

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