greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

bump gameserver after fixes

Browse Source
This commit is contained in:
Jon Eugster
2023-08-12 12:35:29 +02:00
parent 15e854f991
commit b41a35d56c
20 changed files with 32 additions and 204 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
Game.lean
View File

@@ -64,9 +64,9 @@ If you delete it, your progress will be lost!
"
-- Add manual paths
--Dependency Addition → Multiplication → Power
Dependency Addition → Multiplication → Power
Dependency Addition → AdvAddition → AdvMultiplication → Inequality → Prime → Hard
Dependency Multiplication → AdvMultiplication
--Dependency AdvAddition → Evendd → Inequality → StrongInduction
Dependency AdvAddition → EvenOdd → Inequality → StrongInduction
MakeGame

2
Game/Levels/AdvAddition.lean
View File

@@ -1,6 +1,4 @@
import Game.Levels.Addition
import Game.Levels.AdvAddition.placeholder
World "AdvAddition"
Title "Advanced Addition World"

23
Game/Levels/AdvAddition/placeholder.lean
View File

@@ -1,23 +0,0 @@
import Game.Levels.Addition
World "AdvAddition"
Level 1
Title "dunno yet"
open MyNat
Introduction
"
placeholder
"
/-- hello mum -/
Statement
(a : ℕ) : a = a := by
rfl
Conclusion
"
placeholder
"

2
Game/Levels/AdvMultiplication.lean
View File

@@ -1,7 +1,5 @@
import Game.Levels.Multiplication
import Game.Levels.AdvAddition
import Game.Levels.AdvMultiplication.placeholder
World "AdvMultiplication"
Title "Advanced Multiplication World"

24
Game/Levels/AdvMultiplication/placeholder.lean
View File

@@ -1,24 +0,0 @@
import Game.Levels.Multiplication
import Game.Levels.AdvAddition
World "AdvMultiplication"
Level 1
Title "dunno yet"
open MyNat
Introduction
"
placeholder for advanced multiplication world
"
/-- hello mum -/
Statement
(a : ℕ) : a = a := by
rfl
Conclusion
"
placeholder
"

8
Game/Levels/EvenOdd.lean
View File

@@ -1 +1,7 @@
import Game.Levels.EvenOdd.placeholder
import GameServer.Commands
World "EvenOdd"
Title "Parity World"
Introduction
""

23
Game/Levels/EvenOdd/placeholder.lean
View File

@@ -1,23 +0,0 @@
import Game.Levels.Addition
World "EvenOdd"
Level 1
Title "dunno yet"
open MyNat
Introduction
"
placeholder
"
/-- hello mum -/
Statement
(a : ℕ) : a = a := by
rfl
Conclusion
"
placeholder
"

8
Game/Levels/Hard.lean
View File

@@ -1 +1,7 @@
import Game.Levels.Hard.placeholder
import GameServer.Commands
World "Hard"
Title "Impossible World"
Introduction
""

22
Game/Levels/Hard/placeholder.lean
View File

@@ -1,22 +0,0 @@
import Game.Levels.Prime
World "Hard"
Level 1
Title "dunno yet"
open MyNat
Introduction
"
placeholder
"
/-- hello mum -/
Statement
(a : ℕ) : a = a := by
rfl
Conclusion
"
placeholder
"

3
Game/Levels/Inequality.lean
View File

@@ -1,4 +1,5 @@
import Game.Levels.Inequality.Level_1
import GameServer.Commands
-- import Game.Levels.Inequality.Level_1
-- import Game.Levels.Inequality.Level_2
-- import Game.Levels.Inequality.Level_3
-- import Game.Levels.Inequality.Level_4

1
Game/Levels/Multiplication.lean
View File

@@ -1,5 +1,4 @@
import Game.Levels.Addition
import Game.Levels.Multiplication.placeholder
World "Multiplication"
Title "Multiplication World"

23
Game/Levels/Multiplication/placeholder.lean
View File

@@ -1,23 +0,0 @@
import Game.Levels.Addition
World "Multiplication"
Level 1
Title "dunno yet"
open MyNat
Introduction
"
placeholder
"
/-- hello mum -/
Statement
(a : ℕ) : a = a := by
rfl
Conclusion
"
placeholder
"

1
Game/Levels/Power.lean
View File

@@ -1,5 +1,4 @@
import Game.Levels.Multiplication
import Game.Levels.Power.placeholder
World "Power"
Title "Power World"

23
Game/Levels/Power/placeholder.lean
View File

@@ -1,23 +0,0 @@
import Game.Levels.Multiplication
World "Power"
Level 1
Title "dunno yet"
open MyNat
Introduction
"
placeholder
"
/-- hello mum -/
Statement
(a : ℕ) : a = a := by
rfl
Conclusion
"
placeholder
"

7
Game/Levels/Prime.lean
View File

@@ -1,2 +1,7 @@
import Game.Levels.Inequality
import Game.Levels.Prime.placeholder
World "Prime"
Title "Prime World"
Introduction
""

23
Game/Levels/Prime/placeholder.lean
View File

@@ -1,23 +0,0 @@
import Game.Levels.Inequality
World "Prime"
Level 1
Title "dunno yet"
open MyNat
Introduction
"
placeholder
"
/-- hello mum -/
Statement
(a : ℕ) : a = a := by
rfl
Conclusion
"
placeholder
"

7
Game/Levels/StrongInduction.lean
View File

@@ -1,2 +1,7 @@
import Game.Levels.Inequality
import Game.Levels.StrongInduction.placeholder
World "StrongInduction"
Title "Strong Induction World"
Introduction
""

23
Game/Levels/StrongInduction/placeholder.lean
View File

@@ -1,23 +0,0 @@
import Game.Levels.Inequality
World "StrongInduction"
Level 1
Title "dunno yet"
open MyNat
Introduction
"
placeholder
"
/-- hello mum -/
Statement
(a : ℕ) : a = a := by
rfl
Conclusion
"
placeholder
"

7
lake-manifest.json
View File

@@ -31,12 +31,7 @@
"rev": "354432d437fb37738ed93ac6988669d78a870ed0",
"name": "aesop",
"inputRev?": "master"}},
{"git":
{"url": "https://github.com/leanprover-community/lean4game.git",
"subDir?": "server",
"rev": "adb93e30bd0c0364a91b7ee4c606a01d33c5acd4",
"name": "GameServer",
"inputRev?": "adb93e30bd0c0364a91b7ee4c606a01d33c5acd4"}},
{"path": {"name": "GameServer", "dir": "./../lean4game/server"}},
{"git":
{"url": "https://github.com/leanprover/std4",
"subDir?": null,

2
lakefile.lean
View File

@@ -8,7 +8,7 @@ def LocalGameServer : Dependency := {
def RemoteGameServer : Dependency := {
name := `GameServer
src := Source.git "https://github.com/leanprover-community/lean4game.git" "adb93e30bd0c0364a91b7ee4c606a01d33c5acd4" "server"
src := Source.git "https://github.com/leanprover-community/lean4game.git" "70d30d121248723c5170adcafdaf91f3277a069b" "server"
}
/- Choose dependency depending on the environment variable NODE_ENV -/