6. Preview Relationships
Target statement with associated Lean code.
Lean code for Definition6.1●1 definition
Associated Lean declarations
-
Nat.add[complete]
-
Nat.add[complete]
-
defdefined in Init/Prelude.leancomplete
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.
Auxiliary target statement for multi-use proof previews.
Statement depends on Definition 6.1.
- No associated Lean code or declarations.
Statement facet marker for preview relationships.
Proof facet marker for preview relationships, depending on Definition 6.1.
- No associated Lean code or declarations.
Statement facet for a proof with multiple dependencies.
Proof panel marker for preview relationships, also depending on Definition 6.2.
Grouped statement facet with group, used-by, and Lean metadata.
Lean code for Theorem6.6●1 definition
Associated Lean declarations
-
Nat.add[complete]
-
Nat.add[complete]
-
defdefined in Init/Prelude.leancomplete
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.
Grouped proof panel marker for preview relationships, also depending on Definition 6.2.
Consumer statement that makes the grouped statement used-by and group chips non-empty.
- No associated Lean code or declarations.
Statement facet marker for preview relationships.
Proof facet marker for preview relationships.
Available prepared resource body.
This cached body retains cached blank reference and cached available reference.
This single dependency retains its link: blank target.
A second dependency has a body: available target.
Explicit references retain their presentation: blank reference and available reference.