this should disable zero-ne-succ

leanprover-community · Mar 17, 2024 · 0934f62 · 0934f62
1 parent 61ce832
commit 0934f62
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/Game/Levels/Algorithm/L06is_zero.lean b/Game/Levels/Algorithm/L06is_zero.lean
@@ -61,3 +61,5 @@ Statement succ_ne_zero (a : ℕ) : succ a ≠ 0 := by
   rw [h]
   rw [is_zero_zero]
   triv
+
+DisabledTheorem MyNat.zero_ne_succ