upgrade and level typos

README.md

@@ -2,7 +2,7 @@
 
 This is a prototype for a Lean 4 game platform. It is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
 (NNG)](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)
-of Kevin Buzzard and Mohammad Pedramfar. 
+of Kevin Buzzard and Mohammad Pedramfar.
 The project is currently mostly copied from Patrick Massot's [NNG4](https://github.com/PatrickMassot/NNG4), but we plan to extend it significantly.
 
 Building this requires a [npm](https://www.npmjs.com/) toolchain. After cloning the repository you should run
@@ -26,3 +26,21 @@ On the server side, the command will set up a docker image containing the Lean s
 
 Providing the use access to a Lean instance running on the server is a severe security risk. That is why we start the Lean server in a Docker container
 secured by [gVisor](https://gvisor.dev/).
+
+
+## Detailed installation notes
+
+### Node.js
+
+Developed using `node v18.12.1 (npm v8.19.2)`.
+
+Install `nvm`
+```
+curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.2/install.sh | bash
+```
+then reopen bash and test with `command -v nvm` if it is available (Should print "nvm").
+
+Now install node:
+```
+nvm install node --lts
+```

server/testgame/TestGame/Levels/Logic/L01_Rfl.lean

@@ -11,7 +11,7 @@ Introduction
 Willkommen zum Lean-Crashkurs wo du lernst wie man mathematische Beweise vom Computer
 unterstützt und verifiziert schreiben kann.
 
-*Rechts* siehst den Status des Beweis. Unter **Main Goal** steht, was du im Moment am Beweisen
+*Rechts* siehst den Status des Beweis. Unter **Main Goal** steht, was du im Moment am beweisen
 bist. Falls es mehrere Subgoals gibt, werden alle weiteren darunter unter **Further Goals**
 aufgelistet, diese musst du dann später auch noch zeigen.
 
@@ -35,6 +35,6 @@ Message : 42 = 42 =>
 Hint : 42 = 42 =>
 "Man schreibt eine Taktik pro Zeile, also gib `rfl` ein und geh mit Enter ⏎ auf eine neue Zeile."
 
-Conclusion "Bravo!"
+Conclusion "Bravo! PS: `rfl` steht für \"reflexivity\"."
 
 Tactics rfl

server/testgame/TestGame/Levels/Logic/L05c_Apply.lean

@@ -23,10 +23,13 @@ Statement
   assumption
 
 Message (A : Prop) (B : Prop) (C : Prop) (f : A → B) (g : B → C) : A → C =>
-"Mit `intro hA` kann man eine Implikation angehen."
+"Mit `intro hA` kann man annehmen, dass $A$ wahr ist. danach muss man $B$ zeigen."
 
 Message (A : Prop) (B : Prop) (C : Prop) (hA : A) (f : A → B) (g : B → C) : C =>
 "Jetzt ist es ein altbekanntes Spiel von `apply`-Anwendungen."
 
+Hint (A : Prop) (B : Prop) (C : Prop) (hA : A) (f : A → B) (g : B → C) : C =>
+"Du willst $C$ beweisen. Suche also nach einer Implikation $\\ldots \\Rightarrow C$ und wende
+diese mit `apply` an."
 
 Tactics intro apply assumption

server/testgame/TestGame/Levels/Logic/L06b_Iff.lean

@@ -11,7 +11,7 @@ Introduction
 Ein $A \\iff B$ besteht intern aus zwei Implikationen, $\\textrm{mp} : A \\Rightarrow B$
 und $\\textrm{mpr} : B \\Rightarrow A$.
 
-Wenn man ein `A ↔ B` im Goal hat, kann man dieses mit `constructor` in die
+Wenn man ein `A ↔ B` zeigen will (im Goal), kann man dieses mit `constructor` in die
 Einzelteile zerlegen.
 "
 

server/testgame/TestGame/Levels/Logic/L06c_Iff.lean

@@ -10,7 +10,7 @@ Title "Genau dann wenn"
 
 Introduction
 "
-Wenn man eine Annahme `(h : A ↔ B)` hat, kann man auch davon die Einzelnen
+Wenn man eine Annahme `(h : A ↔ B)` hat, kann man auch davon die beiden einzelnen
 Implikationen $\\textrm{mp} : A \\Rightarrow B$ und $\\textrm{mpr} : B \\Rightarrow A$
 brauchen.