fix "no text on tutorial intro" bug

leanprover-community · Sep 25, 2023 · 707f7c4 · 707f7c4
1 parent 0249d2e
commit 707f7c4
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 5 deletions.
diff --git a/Game/Levels/Addition/L01zero_add.lean b/Game/Levels/Addition/L01zero_add.lean
@@ -1,6 +1,10 @@
 import Game.Metadata
 import Game.MyNat.Addition
-import Game.Levels.Tutorial.L05add_succ
+import Game.MyNat.DecidableEq
+
+-- try to fix tutorial world entry page text issue
+-- import Game.Levels.Tutorial.L05add_succ
+
 World "Addition"
 Level 1
 Title "zero_add"

diff --git a/Game/Levels/Multiplication/L01mul_one.lean b/Game/Levels/Multiplication/L01mul_one.lean
@@ -35,20 +35,16 @@ NewDefinition Mul
 
 LemmaDoc MyNat.mul_zero as "mul_zero" in "Mul"
 "
-
 `mul_zero m` is the proof that `m * 0 = 0`."
 
 LemmaDoc MyNat.mul_succ as "mul_succ" in "Mul"
 "
-
 `mul_succ a b` is the proof that `a * succ b = a * b + a`.
 "
 
 NewLemma MyNat.mul_zero MyNat.mul_succ
 
 LemmaDoc MyNat.mul_one as "mul_one" in "Mul" "
-`mul_one m : m * 1 = m`
-
 `mul_one m` is the proof that `m * 1 = m`.
 "
 

diff --git a/Game/Levels/Tutorial/L03three_eq_sss0.lean b/Game/Levels/Tutorial/L03three_eq_sss0.lean
@@ -78,6 +78,7 @@ LemmaDoc MyNat.four_eq_succ_three as "four_eq_succ_three" in "numerals"
 
 NewLemma MyNat.one_eq_succ_zero MyNat.two_eq_succ_one MyNat.three_eq_succ_two
   MyNat.four_eq_succ_three
+
 LemmaTab "numerals"
 
 Conclusion