fixes

leanprover-community · Oct 14, 2023 · 3648e91 · 3648e91
1 parent f625cb5
commit 3648e91
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 10 deletions.
diff --git a/Game/Tactic/Induction.lean b/Game/Tactic/Induction.lean
@@ -3,11 +3,6 @@ import Lean.Elab.Tactic.Induction
 import Std.Tactic.OpenPrivate
 import Std.Data.List.Basic
 import Game.MyNat.Definition
-import Lean
-import Std.Tactic.OpenPrivate
-import Std.Data.List.Basic
-import Mathlib.Lean.Expr.Basic
-
 import Mathlib.Lean.Expr.Basic
 
 

diff --git a/Game/Tactic/cases_test.lean b/Game/Tactic/cases_test.lean
@@ -1,18 +1,20 @@
 import Game.Levels.LessOrEqual
 
+namespace MyNat
+
 example (P Q : Prop) (h : P ∨ Q) : False := by
   cases h with hp hq
-  sorry -- hp : P
-  sorry -- hq : Q
+  · sorry -- hp : P
+  · sorry -- hq : Q
 
 example (a b : ℕ) (h : a ≤ b) : False := by
   cases h with c hc
+  -- hc: b = a + c
   sorry
 
 -- not working yet
 example (a : ℕ) : a = a := by
   cases a with d
   -- get MyNat.zero because we used rec not rec' :-(
-  sorry
-
-  sorry
+  · sorry
+  · sorry