Skip to content

Commit

Permalink
bump to v4.3.0; implementing images
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster committed Dec 8, 2023
1 parent 757a88f commit 8675850
Show file tree
Hide file tree
Showing 6 changed files with 18 additions and 7 deletions.
9 changes: 9 additions & 0 deletions Game.lean
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,15 @@ Kontakt: [Jon Eugster](https://www.math.hhu.de/lehrstuehle-/-personen-/-ansprech
Conclusion
"Fertig!"


/-! Information to be displayed on the servers landing page. -/
Languages "English"
CaptionShort "Game Template"
CaptionLong "You should use this game as a template for your own game and add your own levels."
-- Prerequisites "" -- add this if your game depends on other games
CoverImage "images/cover.png"

Dependency Inequality → SetTheory

/-! Build the game. Show's warnings if it found a problem with your game. -/
MakeGame
2 changes: 2 additions & 0 deletions Game/Levels/Proposition.lean
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,8 @@ import Game.Levels.Proposition.L13_Summary
World "Proposition"
Title "Logo"

Image "images/planet_logos.jpg"

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.
Expand Down
Binary file added images/cover.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added images/planet_logos.jpg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
12 changes: 6 additions & 6 deletions lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down Expand Up @@ -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",
Expand Down
2 changes: 1 addition & 1 deletion lean-toolchain
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:v4.3.0-rc2
leanprover/lean4:v4.3.0

0 comments on commit 8675850

Please sign in to comment.