Merge pull request #65 from yannickseurin/typos

Typos in "Power" world
leanprover-community · Jun 13, 2024 · bed66ee · bed66ee
2 parents 401d973 + 47e143c
commit bed66ee
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/Game/Levels/Power/L07mul_pow.lean b/Game/Levels/Power/L07mul_pow.lean
@@ -11,7 +11,7 @@ Introduction
 The music gets ever more dramatic, as we explore
 the interplay between exponentiation and multiplication.
 
-If you're having trouble exchanging the right `x * y`
+If you're having trouble exchanging the right `a * b`
 because `rw [mul_comm]` swaps the wrong multiplication,
 then read the documentation of `rw` for tips on how to fix this.
 "

diff --git a/Game/Levels/Power/L08pow_pow.lean b/Game/Levels/Power/L08pow_pow.lean
@@ -39,7 +39,7 @@ Conclusion
 The music dies down. Is that it?
 
 Course it isn't, you can
-clearly see that there are two worlds left.
+clearly see that there are two levels left.
 
 A passing mathematician says that mathematicians don't have a name
 for the structure you just constructed. You feel cheated.