Blueprint Lean Code Link Preview Wiring
Definition12
✓L∃∀N
used by 0
Associated Lean declarations
-
Nat.add[complete]
Statement with an associated Lean declaration link in the summary.
Lean code for Definition12●1 definition
Associated Lean declarations
-
Nat.add[complete]
Associated Lean declarations
-
Nat.add[complete]
-
def Nat.add
Nat.add : Nat → Nat → NatAddition 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.: NatNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.→ NatNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.→ NatNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.def Nat.add
Nat.add : Nat → Nat → NatAddition 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.: NatNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.→ NatNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.→ NatNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.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.