Manual Side-by-Side Blueprint Graft

 Manual Side-by-Side Blueprint Graft🔗

Compiled2026-07-01T21:39:37ZProject5f17f8aMerge pull request #222 from leanprover/chore/reference-blueprints-catalog-all-v4.30.0-v4.31.0Leanleanprover/lean4:v4.31.0VersoBlueprint5f17f8a
Definition2
uses 0
Used by 2
Reverse dependency previews
Preview
Theorem 3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
EffortsmallTagsgraftsource

Manual left graft body with inline math x + y = y + x and an attached Lean preview.

Lean code for Definition2●1 definition
  • defdefined in VersoBlueprintTests/BlueprintGraft.lean
    complete
    def Verso.VersoBlueprintTests.BlueprintGraft.graftManualLeftValue : Nat
    def Verso.VersoBlueprintTests.BlueprintGraft.graftManualLeftValue :
  Nat
Theorem3
uses 1used by 1XL∃∀N
Priorityhigh

The grafted theorem states (a + b) + c = a + (b + c).

Proof for Theorem 3
uses 0

The proof graft records the same goal and keeps the proof facet selectable.

Definition4
Statement uses 2
Statement dependency previews
Preview
Definition 2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0XL∃∀N

Manual right graft body references Definition 2 and includes display math: \sum_{i=0}^{n} i = n.

DefinitionFeatured definition
Used by 2
Reverse dependency previews
Preview
Theorem 3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
EffortsmallTagsgraftsource

Manual left graft body with inline math x + y = y + x and an attached Lean preview.

Lean code for DefinitionFeatured definition●1 definition
  • defdefined in VersoBlueprintTests/BlueprintGraft.lean
    complete
    def Verso.VersoBlueprintTests.BlueprintGraft.graftManualLeftValueVerso.VersoBlueprintTests.BlueprintGraft.graftManualLeftValue : Nat : 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 Verso.VersoBlueprintTests.BlueprintGraft.graftManualLeftValueVerso.VersoBlueprintTests.BlueprintGraft.graftManualLeftValue : Nat :
  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.
Priorityhigh

The grafted theorem states (a + b) + c = a + (b + c).

The proof graft records the same goal and keeps the proof facet selectable.

DefinitionUses view
Statement uses 2
Statement dependency previews
Preview
Theorem 3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.

Manual right graft body references Definition 2 and includes display math: \sum_{i=0}^{n} i = n.