Blueprint Graph State Showcase
Base definition with complete local Lean code.
Lean code for Definition2
Associated Lean declarations
def showcaseBase : Nat := 1
- No associated Lean code or declarations.
Ready statement depending on Definition 2.
- No associated Lean code or declarations.
Blocked statement depending on Definition 3.
- No associated Lean code or declarations.
Statement depends on Definition 2.
Proof also depends on Definition 2.
- No associated Lean code or declarations.
Statement depends on Definition 2.
Proof depends on Definition 3.
Locally started theorem depending on Definition 2.
Lean code for Theorem7
Associated Lean declarations
theorem showcaseIncomplete : True := ⊢ True
All goals completed! 🐙
Locally complete theorem depending on Definition 3.
Lean code for Theorem8
Associated Lean declarations
theorem showcaseLocalDone : True := ⊢ True
All goals completed! 🐙
Fully complete theorem depending on Definition 2.
Lean code for Theorem9
Associated Lean declarations
theorem showcaseFullDone : True := ⊢ True
All goals completed! 🐙
-
Nat.nope[missing declaration]
Missing external declaration sample.
- No associated Lean code or declarations.
Statement depending on Definition 0.
- No associated Lean code or declarations.
Statement depending on [??].