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

add "leave world" explanation

Browse Source
This commit is contained in:
Kevin Buzzard
2023-12-22 15:00:30 +00:00
parent cfe1ae17d5
commit 7b66e800d3
1 changed files with 4 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -68,6 +68,8 @@ 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.
You have finished tutorial world! Now let's move onto Addition World,
and learn the `induction` tactic.
You have finished tutorial world!
Click \"Leave World\" to go back to the
overworld, and select Addition World, where you will learn
about the `induction` tactic.
"