comment out error

leanprover-community · Sep 25, 2023 · f07062e · f07062e
1 parent 8c27d0d
commit f07062e
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/Game/MyNat/AdvAddition.lean b/Game/MyNat/AdvAddition.lean
@@ -3,9 +3,9 @@ import Game.MyNat.Addition
 namespace MyNat
 
 attribute [-simp] MyNat.succ.injEq
-example (a b : ℕ) (h : (succ a) = b) : succ (succ a) = succ b := by
-  simp
-  sorry
+-- example (a b : ℕ) (h : (succ a) = b) : succ (succ a) = succ b := by
+--   simp
+--   sorry
 
 --axiom succ_inj {a b : ℕ} : succ a = succ b → a = b