4. Preview Relationships
Definition4.1
✓L∃∀N
Associated Lean declarations
-
Nat.add[complete]
Used by 2
Preview
Lemma 4.2
Target statement with associated Lean code.
Lean code for Definition4.1●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.
Lemma4.2
XL∃∀N
used by 0
Lean status
- No associated Lean code or declarations.
Statement depends on Definition 4.1.
Theorem4.3
XL∃∀N
used by 0
Lean status
- No associated Lean code or declarations.
Statement facet marker for preview relationships.
Proof
Proof facet marker for preview relationships, depending on Definition 4.1.
Theorem4.4
XL∃∀N
used by 0
Lean status
- No associated Lean code or declarations.
Statement facet marker for preview relationships.
Proof
Proof facet marker for preview relationships.