Merge pull request #47 from Not-Abram/ReturnToTypewriterModeSuggestion

Return to typewriter mode suggestion
leanprover-community · Feb 2, 2024 · d24f07d · d24f07d
2 parents bc38caf + b248e1c
commit d24f07d
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/Game/Levels/Addition/L01zero_add.lean b/Game/Levels/Addition/L01zero_add.lean
@@ -28,6 +28,9 @@ will ask us to show that if `0 + d = d` then `0 + succ d = succ d`. Because
 `0` and successor are the only way to make numbers, this will cover all the cases.
 
 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 in the top right.)
 "
 
 /--

diff --git a/Game/Levels/Tutorial/L08twoaddtwo.lean b/Game/Levels/Tutorial/L08twoaddtwo.lean
@@ -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