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