remove excessive import

leanprover-community · Nov 12, 2023 · f33eb30 · f33eb30
1 parent 5cfeac8
commit f33eb30
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/Game/MyNat/DecidableEq.lean b/Game/MyNat/DecidableEq.lean
@@ -1,7 +1,6 @@
 import Game.MyNat.PeanoAxioms
 import Game.Levels.Algorithm.L07succ_ne_succ -- succ_ne_succ
-import Mathlib.Tactic
-import Game.Tactic.decide
+import Game.Tactic.decide -- modified decide tactic
 
 namespace MyNat