desperate attempt to avoid "no text in level intro world" bug

leanprover-community · Oct 12, 2023 · 78a0b03 · 78a0b03
1 parent e86866b
commit 78a0b03
Show file tree

Hide file tree

Showing 3 changed files with 0 additions and 4 deletions.
diff --git a/Game/Levels/AdvAddition.lean b/Game/Levels/AdvAddition.lean
@@ -1,4 +1,3 @@
-import Game.Levels.Implication
 import Game.Levels.AdvAddition.L01ne_succ_self
 import Game.Levels.AdvAddition.L02add_right_cancel
 import Game.Levels.AdvAddition.L03add_left_cancel

diff --git a/Game/Levels/Implication.lean b/Game/Levels/Implication.lean
@@ -1,5 +1,3 @@
-import Game.Levels.Addition
-import Game.MyNat.PeanoAxioms -- `zero_ne_succ` and `succ_inj`
 import Game.Levels.Implication.L01exact
 import Game.Levels.Implication.L02exact2
 import Game.Levels.Implication.L03apply

diff --git a/Game/Levels/Power.lean b/Game/Levels/Power.lean
@@ -1,4 +1,3 @@
-import Game.Levels.Multiplication
 import Game.Levels.Power.L01zero_pow_zero
 import Game.Levels.Power.L02zero_pow_succ
 import Game.Levels.Power.L03pow_one