empty files of glimpse of lean

.i18n/en/Game.pot

@@ -1,7 +1,7 @@
 msgid ""
 msgstr "Project-Id-Version: Game v4.7.0\n"
 "Report-Msgid-Bugs-To: \n"
-"POT-Creation-Date: Wed Apr 10 15:31:40 2024\n"
+"POT-Creation-Date: Sat Aug 17 20:04:45 2024\n"
 "Last-Translator: \n"
 "Language-Team: none\n"
 "Language: en\n"

Game.lean

@@ -1,20 +1,19 @@
-import Game.Levels.DemoWorld
+import GameServer.Commands
 
--- Here's what we'll put on the title screen
-Title "Hello World Game"
-Introduction
-"
-This text appears on the starting page where one selects the world/level to play.
-You can use markdown.
-"
+-- import all worlds
+import Game.Levels.Introduction
+import Game.Levels.Basics
+import Game.Levels.Topics
 
-Info "
-Here you can put additional information about the game. It is accessible
-from the starting through the drop-down menu.
+Title "GlimpseOfLean Game"
 
-For example: Game version, Credits, Link to Github and Zulip, etc.
+Introduction "
+Welcome to the GlimpseOfLean game! This game is designed to introduce you to theorem proving in Lean.
+Click on a world to start.
+"
 
-Use markdown.
+Info "
+This game has been developed to give you a glimpse of Lean in a couple of hours.
 "
 
 /-! Information to be displayed on the servers landing page. -/

Game/Levels/Basics.lean

@@ -0,0 +1,12 @@
+import Game.Levels.Basics.L01_Rewriting
+import Game.Levels.Basics.L02_Iff
+import Game.Levels.Basics.L03_Forall
+import Game.Levels.Basics.L04_Exists
+
+World "Basics"
+Title "Basics World"
+
+Introduction
+"
+This introduction text is shown when one first enters the Basics World.
+"

Game/Levels/Introduction.lean

@@ -0,0 +1,9 @@
+import Game.Levels.Introduction.L01_Introduction
+
+World "Introduction"
+Title "Introduction World"
+
+Introduction
+"
+This introduction text is shown when one first enters the Introduction World.
+"

Game/Levels/DemoWorld.lean → Game/Levels/Introduction/L01_Introduction.lean

@@ -1,6 +1,6 @@
-import Game.Levels.DemoWorld.L01_HelloWorld
-
+import Game.Metadata
 World "DemoWorld"
+Level 1
 Title "Demo World"
 
 Introduction "

Game/Levels/Topics.lean

@@ -0,0 +1,13 @@
+import Game.Levels.Topics.L01_ChineseRemainder
+import Game.Levels.Topics.L02_ClassicalPropositionalLogic
+import Game.Levels.Topics.L03_GaloisAdjunctions
+import Game.Levels.Topics.L04_IntuitionisticPropositionalLogic
+import Game.Levels.Topics.L05_SequenceLimits
+
+World "Topics"
+Title "Topics World"
+
+Introduction
+"
+This introduction text is shown when one first enters the Topics World.
+"