Lean Auto Dependencies
Inspect auto.demo.statement_target for a statement panel with one automatic
edge and one manual edge, auto.demo.proof_target for the same split on a
proof panel, and auto.demo.excluded_target for an automatic edge removed by
an attribute exclusion. This file also enables
set_option verso.blueprint.autoDeps true for the examples that use
(lean := "...") and inline Lean code. Inference follows unassociated helpers
by default.
Tagged source declaration used by another declaration's type. Edges to this node can pass through unassociated type aliases without giving those aliases nodes.
Lean code for Definition1●1 definition
Associated Lean declarations
-
defdefined in VersoBlueprintTests/BlueprintAutoDeps/Preview.leancomplete
def Verso.VersoBlueprintTests.BlueprintAutoDeps.Preview.autoDemoTypeSource : Prop
def Verso.VersoBlueprintTests.BlueprintAutoDeps.Preview.autoDemoTypeSource : Prop
Tagged source theorem used by another declaration's proof. Edges to this node should appear on proof dependency chips, not statement dependency chips.
Lean code for Theorem2●1 theorem
Associated Lean declarations
-
theoremdefined in VersoBlueprintTests/BlueprintAutoDeps/Preview.leancomplete
theorem Verso.VersoBlueprintTests.BlueprintAutoDeps.Preview.autoDemoProofSource : True
theorem Verso.VersoBlueprintTests.BlueprintAutoDeps.Preview.autoDemoProofSource : True
Manual comparison dependency. This edge is written in the attribute options, so it should stay manual while inferred edges are marked automatic.
Lean code for Theorem3●1 theorem
Associated Lean declarations
-
theoremdefined in VersoBlueprintTests/BlueprintAutoDeps/Preview.leancomplete
theorem Verso.VersoBlueprintTests.BlueprintAutoDeps.Preview.autoDemoManualExtra : True
theorem Verso.VersoBlueprintTests.BlueprintAutoDeps.Preview.autoDemoManualExtra : True
The Lean statement uses autoDemoTypeAlias, which leads to autoDemoTypeSource,
so automatic dependency inference adds auto.demo.type_source. The attribute also adds
auto.demo.manual_extra manually, making the statement dependency panel show
both origins side by side.
Lean code for Theorem4●1 theorem
Associated Lean declarations
-
theoremdefined in VersoBlueprintTests/BlueprintAutoDeps/Preview.leancomplete
theorem Verso.VersoBlueprintTests.BlueprintAutoDeps.Preview.autoDemoStatementTarget : autoDemoTypeAlias
theorem Verso.VersoBlueprintTests.BlueprintAutoDeps.Preview.autoDemoStatementTarget : autoDemoTypeAlias
The Lean statement is just True, so there is no inferred statement dependency.
The proof below reaches autoDemoProofSource through autoDemoProofHelper.
Lean code for Theorem5●1 theorem
Associated Lean declarations
-
theoremdefined in VersoBlueprintTests/BlueprintAutoDeps/Preview.leancomplete
theorem Verso.VersoBlueprintTests.BlueprintAutoDeps.Preview.autoDemoProofTarget : True
theorem Verso.VersoBlueprintTests.BlueprintAutoDeps.Preview.autoDemoProofTarget : True
The Lean proof body reaches autoDemoProofSource through a helper, so automatic dependency
inference adds auto.demo.proof_source to the proof dependencies. The attribute
also adds auto.demo.manual_extra manually for comparison.
The Lean statement mentions autoDemoTypeSource, but the attribute excludes
auto.demo.type_source. Only the manually listed auto.demo.manual_extra
dependency remains.
Lean code for Theorem6●1 theorem
Associated Lean declarations
-
theoremdefined in VersoBlueprintTests/BlueprintAutoDeps/Preview.leancomplete
theorem Verso.VersoBlueprintTests.BlueprintAutoDeps.Preview.autoDemoExcludedTarget : autoDemoTypeSource
theorem Verso.VersoBlueprintTests.BlueprintAutoDeps.Preview.autoDemoExcludedTarget : autoDemoTypeSource
This node points at an existing compiled Lean declaration with (lean := ...).
The file option enables automatic dependencies, so the declaration's type and
proof body provide statement and proof edges through the same helpers.
Lean code for Theorem7●1 theorem
Associated Lean declarations
-
autoDemoExternalTargetDecl[complete]
-
autoDemoExternalTargetDecl[complete]
-
theoremdefined in VersoBlueprintTests/BlueprintAutoDeps/Preview.leancomplete
theorem Verso.VersoBlueprintTests.BlueprintAutoDeps.Preview.autoDemoExternalTargetDecl : autoDemoTypeAlias
theorem Verso.VersoBlueprintTests.BlueprintAutoDeps.Preview.autoDemoExternalTargetDecl : autoDemoTypeAlias
This node has an inline Lean block. The file option also enables automatic dependencies for the declarations defined in the block.
Lean code for Definition8
Associated Lean declarations
theorem autoDemoInlineTargetDecl : autoDemoTypeAlias := ⊢ autoDemoTypeAlias
All goals completed! 🐙
This node points at a compiled Lean declaration, but locally disables automatic dependency inference.
Lean code for Theorem9●1 theorem
Associated Lean declarations
-
autoDemoExternalOptOutDecl[complete]
-
autoDemoExternalOptOutDecl[complete]
-
theoremdefined in VersoBlueprintTests/BlueprintAutoDeps/Preview.leancomplete
theorem Verso.VersoBlueprintTests.BlueprintAutoDeps.Preview.autoDemoExternalOptOutDecl : autoDemoTypeSource
theorem Verso.VersoBlueprintTests.BlueprintAutoDeps.Preview.autoDemoExternalOptOutDecl : autoDemoTypeSource
A prose-first node links to the inferred targets with ordinary manual dependencies: Theorem 4, Theorem 5, Theorem 7, and Definition 8.