Ronen Lahat ronenlh
ronenlh
/ infoview4.txt
Created
May 11, 2026 07:34
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Tactic state | |
| No goals | |
| Goals accomplished! |
ronenlh
/ infoview3.txt
Created
May 11, 2026 07:34
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Tactic state | |
| 1 goal | |
| Coin HotWater : Prop | |
| Noodles : Sort ?u.29 | |
| noodleVendingMachine : Coin → HotWater → Noodles | |
| coinAndHotWater : Coin ∧ HotWater | |
| ⊢ Noodles |
ronenlh
/ infoview2.txt
Created
May 11, 2026 07:33
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Tactic state | |
| 1 goal | |
| Coin HotWater : Prop | |
| Noodles : Sort ?u.29 | |
| noodleVendingMachine : Coin → HotWater → Noodles | |
| ⊢ Coin ∧ HotWater → Noodles |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Tactic state | |
| 1 goal | |
| Coin HotWater : Prop | |
| Noodles : Sort ?u.29 | |
| ⊢ (Coin → HotWater → Noodles) → Coin ∧ HotWater → Noodles |
ronenlh
/ check_rfl.lean
Created
May 11, 2026 07:00
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #check rfl | |
| -- rfl.{u} {α : Sort u} {a : α} : a = a |
ronenlh
/ check2_2.lean
Created
May 11, 2026 07:00
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #check 2 + 2 = 4 | |
| -- 2 + 2 = 4 : Prop |
ronenlh
/ check3.lean
Created
May 11, 2026 06:59
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #check Type | |
| -- Type : Type 1 | |
| #check Type 1 | |
| -- Type 1 : Type 2 | |
| -- ... |
ronenlh
/ check2.lean
Created
May 11, 2026 06:59
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #check Nat | |
| -- Nat : Type |
ronenlh
/ check1.lean
Created
May 11, 2026 06:58
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #check 3 | |
| -- 3 : Nat |
ronenlh
/ example_generic.lean
Created
May 11, 2026 06:56
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| example : (P → Q → R) → (P ∧ Q → R) := by | |
| intro h | |
| intro hpq | |
| exact h hpq.left hpq.right |
NewerOlder