add minimal NNG dummy

2023-03-23 16:23:06 +01:00
parent bf2315b474
commit 7992cffa26
5 changed files with 25 additions and 0 deletions
@@ -0,0 +1 @@
+build
@@ -0,0 +1,9 @@
+import GameServer.Commands
+
+Game "NNG"
+World "HelloWorld"
+Level 1
+
+Statement : 1 + 1 = 2 := rfl
+
+MakeGame
@@ -0,0 +1,3 @@
+{"version": 4,
+ "packagesDir": "lake-packages",
+ "packages": [{"path": {"name": "GameServer", "dir": "./../leanserver"}}]}
@@ -0,0 +1,11 @@
+import Lake
+open Lake DSL
+
+require GameServer from ".."/"leanserver"
+
+package NNG
+
+@[default_target]
+lean_lib NNG {
+  moreLeanArgs := #["-DautoImplicit=false"]
+}
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-03-09