remove dead code

leanprover-community · Nov 12, 2023 · 0acd296 · 0acd296
1 parent 2bf6c63
commit 0acd296
Showing 1 changed file with 0 additions and 6 deletions.
diff --git a/Game/MyNat/Addition.lean b/Game/MyNat/Addition.lean
@@ -22,9 +22,3 @@ If `a` and `d` are natural numbers, then `add_succ a d` is the proof that
 -/
 @[MyNat_decide]
 axiom add_succ (a d : MyNat) : a + (succ d) = succ (a + d)
-
--- -- don't tell the viewers, we cheat with decide because
--- -- we used axioms to define nat
--- @[MyNat_decide]
--- theorem toNat_add (m n : MyNat) : (m + n).toNat = m.toNat + n.toNat := by
---   induction n <;> simp [MyNat_decide, Nat.add_succ, *];