Blueprint Graph State Showcase
Definition1
Base definition with complete local Lean code.
Lean code for Definition1
Associated Lean declarations
Associated Lean declarations
def showcaseBase : Nat := 1
Definition2
Ready statement depending on Definition 1.
Definition3
Blocked statement depending on Definition 2.
Theorem4
Statement depends on Definition 1.
Proof for Theorem 4
Proof also depends on Definition 1.
Theorem5
Statement depends on Definition 1.
Proof for Theorem 5
Proof depends on Definition 2.
Locally started theorem depending on Definition 1.
Lean code for Theorem6
Associated Lean declarations
Associated Lean declarations
theorem showcaseIncomplete : True := ⊢ True
All goals completed! 🐙
Locally complete theorem depending on Definition 2.
Lean code for Theorem7
Associated Lean declarations
Associated Lean declarations
theorem showcaseLocalDone : True := ⊢ True
All goals completed! 🐙
Fully complete theorem depending on Definition 1.
Lean code for Theorem8
Associated Lean declarations
Associated Lean declarations
theorem showcaseFullDone : True := ⊢ True
All goals completed! 🐙
Definition9
Missing external declaration sample.
Lemma10
Statement depending on def:showcase.lean_only.