1. Core Previews
Definition1.1
Group: Core statements that drive the showcase summary and dependency graph. (3)
Preview
Lemma 1.2
Lean status
- No associated Lean code or declarations.
Base statement for summary and graph previews.
Lemma1.2
Group: Core statements that drive the showcase summary and dependency graph. (3)
Preview
Definition 1.1
Lean status
- No associated Lean code or declarations.
Depends on Definition 1.1.
Definition1.3
Statement with an associated Lean declaration link in the summary.
Lean code for Definition1.3●1 definition
Associated Lean declarations
-
Nat.add[complete]
Associated Lean declarations
-
Nat.add[complete]
-
defdefined in Init/Prelude.leancomplete
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.
Theorem1.4
Group: Core statements that drive the showcase summary and dependency graph. (3)
Preview
Definition 1.1
Lean status
- No associated Lean code or declarations.
Combines Lemma 1.2 with Definition 1.3.