From cdea03781cc064a140eeebc281f1b4b5c5f4609f Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 6 Mar 2023 16:30:43 +0100 Subject: [PATCH] levels --- server/testgame/TestGame.lean | 17 ++------------ .../testgame/TestGame/Levels/Implication.lean | 14 +++++++++++ .../testgame/TestGame/Levels/Proposition.lean | 21 +++++++++++++++++ .../Levels/Proposition/L00_Tauto.lean | 23 +------------------ 4 files changed, 38 insertions(+), 37 deletions(-) diff --git a/server/testgame/TestGame.lean b/server/testgame/TestGame.lean index 1669b22..a6d5646 100644 --- a/server/testgame/TestGame.lean +++ b/server/testgame/TestGame.lean @@ -23,22 +23,9 @@ Game "TestGame" Title "Lean 4 game" Introduction " -Durch eine unvorhergesehene und nicht-kanonische Singularität in der Raumzeit -bist Du ausversehen in ein Paralleluniversum gestolpert. Wie es aussieht, gibt es kein zurück. -Richte Dich besser darauf ein, hier bleiben und Dich zurechtzufinden zu müssen. - -Wie es aussieht, gibt es hier viele nette kleine Planeten. Alle bewohnbar, und bis zu -sieben Sonnenuntergänge täglich inklusive. Nur werden sie allesamt von Formalosophen bewohnt, -seltsamen Wesen mit ausgefallenen mathematischen Obsessionen. Und dummerweise hat sich -herumgesprochen, dass Du in Deinem früheren Universum Mathematiker warst. Du wirst hier -keine Ruhe finden, solange Du nicht lernst, ihren unablässigen Wissensdurst zu stillen. - -Es gibt nur zwei Schwierigkeiten: Erstens haben die Formalosophen allem Anschein nach -überhaupt kein tieferes mathematisches Verständnis, und zweitens kommunizieren Sie -exklusiv in einem Dir fremden Dialekt. Zum Glück hat Robo mit Dir das Universum gewechselt. -Robo, das ist Dein kleiner SmartElf. Robo kann zwar auch keine Mathematik, aber es scheint, -er kann irgendetwas mit dem Formalosophendialekt anfangen. +TODO " + Conclusion "Fertig!" diff --git a/server/testgame/TestGame/Levels/Implication.lean b/server/testgame/TestGame/Levels/Implication.lean index 9c69a80..4c211af 100644 --- a/server/testgame/TestGame/Levels/Implication.lean +++ b/server/testgame/TestGame/Levels/Implication.lean @@ -14,3 +14,17 @@ import TestGame.Levels.Implication.L12_Summary Game "TestGame" World "Implication" Title "Aussagenlogik 2" + +Introduction +" +Zurück im Raumschiff macht ihr euch auf den Weg zum einem der beiden Monde, die ebenfalls +beide bewohnt zu sein scheinen. + +**Du**: Sag mal Robo, Königin *Logisindes* hat under anderem von Implikationen gesprochen, +aber niemand von den Einwohnern... + +**Robo**: Auf dem Mond *Implis* den wir gerade ansteuern können sie uns vielleicht mehr +erzählen… + +Und damit leitet Robo den Landeanflug ein. +" diff --git a/server/testgame/TestGame/Levels/Proposition.lean b/server/testgame/TestGame/Levels/Proposition.lean index 52058b7..bf6ec84 100644 --- a/server/testgame/TestGame/Levels/Proposition.lean +++ b/server/testgame/TestGame/Levels/Proposition.lean @@ -16,3 +16,24 @@ import TestGame.Levels.Proposition.L13_Summary Game "TestGame" World "Proposition" Title "Aussagenlogik 1" + +Introduction " +Durch eine unvorhergesehene und nicht-kanonische Singularität in der Raumzeit +bist Du ausversehen in ein Paralleluniversum gestolpert. Wie es aussieht, gibt es kein zurück. +Richte Dich besser darauf ein, hier bleiben und Dich zurechtzufinden zu müssen. + +Wie es aussieht, gibt es hier viele nette kleine Planeten. Alle bewohnbar, und bis zu +sieben Sonnenuntergänge täglich inklusive. Nur werden sie allesamt von Formalosophen bewohnt, +seltsamen Wesen mit ausgefallenen mathematischen Obsessionen. Und dummerweise hat sich +herumgesprochen, dass Du in Deinem früheren Universum Mathematiker warst. Du wirst hier +keine Ruhe finden, solange Du nicht lernst, ihren unablässigen Wissensdurst zu stillen. + +Es gibt nur zwei Schwierigkeiten: Erstens haben die Formalosophen allem Anschein nach +überhaupt kein tieferes mathematisches Verständnis, und zweitens kommunizieren Sie über Mathematik +exklusiv in einem Dir fremden Dialekt, den sie Leansch [liːnʃ] nennen. + +Zum Glück hat Robo mit Dir das Universum gewechselt. +Robo, das ist Dein kleiner SmartElf. Robo ist war auch nicht die mathematische Leuchte, die Du Dir +in dieser Situation gewünscht hättest, aber es scheint, er hat irgendwo Leansch gelernt. +Und das ist Gold wert. +" diff --git a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean index 1fced37..99ca026 100644 --- a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean +++ b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean @@ -9,27 +9,6 @@ Title "Automatisierung" Introduction " -Durch eine unvorhergesehene und nicht-kanonische Singularität in der Raumzeit -bist Du ausversehen in ein Paralleluniversum gestolpert. Wie es aussieht, gibt es kein zurück. -Richte Dich besser darauf ein, hier bleiben und Dich zurechtzufinden zu müssen. - -Wie es aussieht, gibt es hier viele nette kleine Planeten. Alle bewohnbar, und bis zu -sieben Sonnenuntergänge täglich inklusive. Nur werden sie allesamt von Formalosophen bewohnt, -seltsamen Wesen mit ausgefallenen mathematischen Obsessionen. Und dummerweise hat sich -herumgesprochen, dass Du in Deinem früheren Universum Mathematiker warst. Du wirst hier -keine Ruhe finden, solange Du nicht lernst, ihren unablässigen Wissensdurst zu stillen. - -Es gibt nur zwei Schwierigkeiten: Erstens haben die Formalosophen allem Anschein nach -überhaupt kein tieferes mathematisches Verständnis, und zweitens kommunizieren Sie über Mathematik -exklusiv in einem Dir fremden Dialekt, den sie Leansch [liːnʃ] nennen. - -Zum Glück hat Robo mit Dir das Universum gewechselt. -Robo, das ist Dein kleiner SmartElf. Robo ist war auch nicht die mathematische Leuchte, die Du Dir -in dieser Situation gewünscht hättest, aber es scheint, er hat irgendwo Leansch gelernt. -Und das ist Gold wert. - ----- - Gerade seid Ihr auf Königin *Logisindes* Planeten. Sie kommt ohne Umschweife zum Punkt: **Logisinde** Werte Wesen aus fremden Welten, gestatten Sie eine Frage. Warum gilt … @@ -48,7 +27,7 @@ Hint (A B C : Prop) : ¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) => "**Robo** Das ist ganz einfach. Mit `{A} {B} {C} : Prop` meint er: `{A}`, `{B}` und `{C}` sind irgendwelche Aussagen (*propositions*). - Und mit `→` meint er ⇒, also “impliziert”. Die anderen Symbole kennst Du, oder? + Und mit `→` meint sie ⇒, also “impliziert”. Die anderen Symbole kennst Du, oder? **Du** Ehhm, ja. Aber da muss ich jetzt trotzdem erst einmal überlegen.