removing unused code

leanprover-community · Nov 12, 2023 · c67e3fb · c67e3fb
1 parent 03d7490
commit c67e3fb
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 5 deletions.
diff --git a/Game/MyNat/Definition.lean b/Game/MyNat/Definition.lean
@@ -41,7 +41,3 @@ def one : MyNat := MyNat.succ 0
 -- TODO: Why does this not work here??
 -- We do not want `simp` to be able to do anything unless we unlock it manually.
 attribute [-simp] MyNat.succ.injEq
-
-theorem eq_toNat_eq : ∀ (m n : MyNat), m.toNat = n.toNat → m = n
-  | zero, zero, _ => rfl
-  | succ m, succ n, h => congrArg succ $ eq_toNat_eq m n (Nat.succ.inj h)
diff --git a/Game/MyNat/PeanoAxioms.lean b/Game/MyNat/PeanoAxioms.lean
@@ -21,7 +21,7 @@ theorem succ_inj (a b : ℕ) (h : succ a = succ b) : a = b := by
 
 def is_zero : ℕ → Prop
 | 0 => True
-| succ n => False
+| succ _ => False
 
 lemma is_zero_zero : is_zero 0 = True := rfl
 lemma is_zero_succ (n : ℕ) : is_zero (succ n) = False := rfl