superficial edit so I can recompile and look at warnings

leanprover-community · Oct 22, 2023 · 674008e · 674008e
1 parent b8e530f
commit 674008e
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Game/Levels/Tutorial/L07add_succ.lean b/Game/Levels/Tutorial/L07add_succ.lean
@@ -6,6 +6,8 @@ World "Tutorial"
 Level 7
 Title "add_succ"
 
+LemmaTab "numerals"
+
 namespace MyNat
 
 LemmaDoc MyNat.add_succ as "add_succ" in "Add"
@@ -48,7 +50,5 @@ Statement succ_eq_add_one n : succ n = n + 1 := by
   Hint (hidden := true) "And finally `rfl`."
   rfl
 
-LemmaTab "numerals"
-
 Conclusion
 "[dramatic music]. Now are you ready to face the first boss of the game?"