From 5b021f5981c877b33682b2acb2e423a255794665 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Thu, 19 Jan 2023 12:17:00 +0100
Subject: [PATCH] Add dummy levels

---
 server/testgame/TestGame.lean                                | 2 ++
 server/testgame/TestGame/Levels/Proposition/L14_Summary.lean | 5 +++--
 server/testgame/TestGame/Levels/Proving.lean                 | 1 +
 .../Levels/Proving/{L03_Contra.lean => L01_Contra.lean}      | 0
 4 files changed, 6 insertions(+), 2 deletions(-)
 create mode 100644 server/testgame/TestGame/Levels/Proving.lean
 rename server/testgame/TestGame/Levels/Proving/{L03_Contra.lean => L01_Contra.lean} (100%)

diff --git a/server/testgame/TestGame.lean b/server/testgame/TestGame.lean
index 140e2db..5dcccfc 100644
--- a/server/testgame/TestGame.lean
+++ b/server/testgame/TestGame.lean
@@ -3,7 +3,9 @@ import TestGame.Metadata
 import TestGame.Levels.Proposition
 import TestGame.Levels.Implication
 import TestGame.Levels.Predicate
+import TestGame.Levels.Proving
 
+import TestGame.Levels.Naturals.L31_Sum
 
 Game "TestGame"
 
diff --git a/server/testgame/TestGame/Levels/Proposition/L14_Summary.lean b/server/testgame/TestGame/Levels/Proposition/L14_Summary.lean
index 2b8896e..7b1f296 100644
--- a/server/testgame/TestGame/Levels/Proposition/L14_Summary.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L14_Summary.lean
@@ -14,10 +14,11 @@ Introduction
 "
 ## Notationen / Begriffe
 
-Damit bist du am Ende der ersten Lektion angekommen. Hier ein Überblick über alle Begriffe und Notationen, die in diesem Kapitel
+Damit bist du am Ende der ersten Lektion angekommen. Hier ein Überblick über alle Begriffe
+und Notationen, die in diesem Kapitel
 eingeführt wurden.
 
-|               | Beschreibung                                                                          |
+|               | Beschreibung                                                             |
 |:--------------|:-------------------------------------------------------------------------|
 | *Goal*        | Was aktuell zu beweisen ist.                                             |
 | *Annahme*     | Objekte & Resultate, die man zur Verfügung hat.                          |
diff --git a/server/testgame/TestGame/Levels/Proving.lean b/server/testgame/TestGame/Levels/Proving.lean
new file mode 100644
index 0000000..e279ac1
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Proving.lean
@@ -0,0 +1 @@
+import TestGame.Levels.Proving.L01_Contra
diff --git a/server/testgame/TestGame/Levels/Proving/L03_Contra.lean b/server/testgame/TestGame/Levels/Proving/L01_Contra.lean
similarity index 100%
rename from server/testgame/TestGame/Levels/Proving/L03_Contra.lean
rename to server/testgame/TestGame/Levels/Proving/L01_Contra.lean