bump to v4.3.0
This commit is contained in:
20
Game.lean
20
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`
|
-- 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
|
MakeGame
|
||||||
|
|||||||
BIN
images/cover.png
Normal file
BIN
images/cover.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 308 KiB |
@@ -4,19 +4,19 @@
|
|||||||
[{"url": "https://github.com/leanprover/std4.git",
|
[{"url": "https://github.com/leanprover/std4.git",
|
||||||
"type": "git",
|
"type": "git",
|
||||||
"subDir": null,
|
"subDir": null,
|
||||||
"rev": "a652e09bd81bcb43ea132d64ecc16580b0c7fa50",
|
"rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087",
|
||||||
"name": "std",
|
"name": "std",
|
||||||
"manifestFile": "lake-manifest.json",
|
"manifestFile": "lake-manifest.json",
|
||||||
"inputRev": "v4.3.0-rc2",
|
"inputRev": "v4.3.0",
|
||||||
"inherited": true,
|
"inherited": true,
|
||||||
"configFile": "lakefile.lean"},
|
"configFile": "lakefile.lean"},
|
||||||
{"url": "https://github.com/leanprover-community/lean4game.git",
|
{"url": "https://github.com/leanprover-community/lean4game.git",
|
||||||
"type": "git",
|
"type": "git",
|
||||||
"subDir": "server",
|
"subDir": "server",
|
||||||
"rev": "622e9d389768e8abb5b3103a65d07165587a27ad",
|
"rev": "d5697d052e5154b909f379073a591ebf66eb3e22",
|
||||||
"name": "GameServer",
|
"name": "GameServer",
|
||||||
"manifestFile": "lake-manifest.json",
|
"manifestFile": "lake-manifest.json",
|
||||||
"inputRev": "v4.3.0-rc2",
|
"inputRev": "v4.3.0",
|
||||||
"inherited": false,
|
"inherited": false,
|
||||||
"configFile": "lakefile.lean"},
|
"configFile": "lakefile.lean"},
|
||||||
{"url": "https://github.com/leanprover-community/quote4",
|
{"url": "https://github.com/leanprover-community/quote4",
|
||||||
@@ -58,10 +58,10 @@
|
|||||||
{"url": "https://github.com/leanprover-community/mathlib4.git",
|
{"url": "https://github.com/leanprover-community/mathlib4.git",
|
||||||
"type": "git",
|
"type": "git",
|
||||||
"subDir": null,
|
"subDir": null,
|
||||||
"rev": "83d4f222771f491b351d70b070406481f5d2b2ba",
|
"rev": "f04afed5ac9fea0e1355bc6f6bee2bd01f4a888d",
|
||||||
"name": "mathlib",
|
"name": "mathlib",
|
||||||
"manifestFile": "lake-manifest.json",
|
"manifestFile": "lake-manifest.json",
|
||||||
"inputRev": "v4.3.0-rc2",
|
"inputRev": "v4.3.0",
|
||||||
"inherited": false,
|
"inherited": false,
|
||||||
"configFile": "lakefile.lean"}],
|
"configFile": "lakefile.lean"}],
|
||||||
"name": "Game",
|
"name": "Game",
|
||||||
|
|||||||
@@ -1 +1 @@
|
|||||||
leanprover/lean4:v4.3.0-rc2
|
leanprover/lean4:v4.3.0
|
||||||
|
|||||||
Reference in New Issue
Block a user