make simp_add available in the entire game #54

leanprover-community · Mar 18, 2024 · c35d29d · c35d29d
1 parent 61ce832
commit c35d29d
Show file tree

Hide file tree

Showing 5 changed files with 40 additions and 395 deletions.
diff --git a/Game/Levels/Algorithm/L04add_algo3.lean b/Game/Levels/Algorithm/L04add_algo3.lean
@@ -1,4 +1,5 @@
 import Game.Levels.Algorithm.L03add_algo2
+import ImportGraph
 
 World "Algorithm"
 Level 4

diff --git a/Game/Metadata.lean b/Game/Metadata.lean
@@ -14,10 +14,7 @@ import Game.Tactic.Rw
 import Game.Tactic.Use
 import Game.Tactic.Ne
 import Game.Tactic.Xyzzy
+import Game.Tactic.SimpAdd
 -- import Std.Tactic.RCases
 -- import Game.Tactic.Have
 -- import Game.Tactic.LeftRight
-
--- 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
diff --git a/Game/Tactic/LeanExprBasic.lean b/Game/Tactic/LeanExprBasic.lean