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.
Tagged source declaration used by another declaration's type. Edges to this node are inferred only when a target's statement mentions the Lean declaration.
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 has type 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 : autoDemoTypeSource
theorem Verso.VersoBlueprintTests.BlueprintAutoDeps.Preview.autoDemoStatementTarget : autoDemoTypeSource
The Lean statement is just True, so there is no inferred statement dependency.
The proof below uses autoDemoProofSource.
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 references autoDemoProofSource, 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.
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 : autoDemoTypeSource
theorem Verso.VersoBlueprintTests.BlueprintAutoDeps.Preview.autoDemoExternalTargetDecl : autoDemoTypeSource
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 : autoDemoTypeSource := ⊢ autoDemoTypeSource
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
- No associated Lean code or declarations.
A prose-first node links to the inferred targets with ordinary manual dependencies: Theorem 4, Theorem 5, Theorem 7, and Definition 8.