greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

add parentheses, consistent language around "modes"

Browse Source
This commit is contained in:
Steven Clontz
2024-01-24 11:33:31 -06:00
committed by GitHub
parent 2112b6c0ac
commit b248e1cca0
2 changed files with 3 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
Game/Levels/Addition/L01zero_add.lean
View File

@@ -29,8 +29,8 @@ will ask us to show that if `0 + d = d` then `0 + succ d = succ d`. Because
See if you can do your first induction proof in Lean.
By the way, if you are still in the editor mode from the last world, you can swap
back to typewriter mode by clicking the `>_` button.
(By the way, if you are still in the \"Editor mode\" from the last world, you can swap
back to \"Typewriter mode\" by clicking the `>_` button in the top right.)
"
/--

2
Game/Levels/Tutorial/L08twoaddtwo.lean
View File

@@ -51,7 +51,7 @@ written as several lines of code. Move your cursor between lines to see
the goal state at any point. Now cut and paste your code elsewhere if you
want to save it, and paste the above proof in instead. Move your cursor
around to investigate. When you've finished, click the `>_` button in the top right to
move back into command line mode.
move back into \"Typewriter mode\".
You have finished tutorial world!
Click \"Leave World\" to go back to the