diff --git a/Game.lean b/Game.lean index fbe3cc5..b494b5f 100644 --- a/Game.lean +++ b/Game.lean @@ -98,16 +98,16 @@ Alternatively, if you experience issues / bugs you can also open github issues: " --- Here's where we show how to glue the worlds together -Dependency Addition → Multiplication → Power ---Dependency Addition → AdvAddition → AdvMultiplication → Inequality → Prime → Hard ---Dependency Multiplication → AdvMultiplication ---Dependency AdvAddition → EvenOdd → Inequality → StrongInduction -Dependency Addition → Implication → AdvAddition → LessOrEqual -Dependency AdvAddition → Algorithm --- The game automatically computes connections between worlds based on introduced --- tactics and theorems, but for example it cannot detect introduced definitions - -- Dependency Implication → Power -- `Power` uses `≠` which is introduced in `Implication` +/-! Information to be displayed on the servers landing page. -/ +Languages "English" +CaptionShort "The classical introduction game for Lean." +CaptionLong "In this game you recreate the natural numbers $\\mathbb{N}$ from the Peano axioms, +learning the basics about theorem proving in Lean. + +This is a good first introduction to Lean!" +CoverImage "images/cover.png" + +/-! Build the game. Show's warnings if it found a problem with your game. -/ MakeGame diff --git a/images/cover.png b/images/cover.png new file mode 100644 index 0000000..69b0df5 Binary files /dev/null and b/images/cover.png differ diff --git a/lake-manifest.json b/lake-manifest.json index 3c7f598..0331f48 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,19 +4,19 @@ [{"url": "https://github.com/leanprover/std4.git", "type": "git", "subDir": null, - "rev": "a652e09bd81bcb43ea132d64ecc16580b0c7fa50", + "rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087", "name": "std", "manifestFile": "lake-manifest.json", - "inputRev": "v4.3.0-rc2", + "inputRev": "v4.3.0", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/lean4game.git", "type": "git", "subDir": "server", - "rev": "622e9d389768e8abb5b3103a65d07165587a27ad", + "rev": "d5697d052e5154b909f379073a591ebf66eb3e22", "name": "GameServer", "manifestFile": "lake-manifest.json", - "inputRev": "v4.3.0-rc2", + "inputRev": "v4.3.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/quote4", @@ -58,10 +58,10 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "83d4f222771f491b351d70b070406481f5d2b2ba", + "rev": "f04afed5ac9fea0e1355bc6f6bee2bd01f4a888d", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.3.0-rc2", + "inputRev": "v4.3.0", "inherited": false, "configFile": "lakefile.lean"}], "name": "Game", diff --git a/lean-toolchain b/lean-toolchain index 24a3cdb..5cadc9d 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.3.0-rc2 +leanprover/lean4:v4.3.0