mynat simp lemmas have 0 in so move from zero to 0

leanprover-community · Nov 1, 2023 · d29d187 · d29d187
1 parent 96be0b3
commit d29d187
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 5 deletions.
diff --git a/Game/MyNat/DecidableEq.lean b/Game/MyNat/DecidableEq.lean
@@ -43,7 +43,6 @@ example : 4 ≠ 5 := by
 example : (0 : ℕ) + 0 = 0 := by
   MyDecide
 
-set_option pp.all true in
 example : (2 : ℕ) + 2 = 4 := by
   MyDecide
 

diff --git a/Game/MyNat/Definition.lean b/Game/MyNat/Definition.lean
@@ -33,11 +33,8 @@ instance instofNat {n : Nat} : OfNat MyNat n where
 instance : ToString MyNat where
   toString p := toString (toNat p)
 
-@[simp]
-theorem zero_eq_0 : MyNat.zero = 0 := rfl
-
 @[MyNat_decide]
-theorem zero_eq_zero : (0 : ℕ) = MyNat.zero := rfl
+theorem zero_eq_0 : MyNat.zero = 0 := rfl
 
 def one : MyNat := MyNat.succ 0