Add World introduction and change layout

2023-03-06 18:07:09 +01:00
parent cdea03781c
commit 75f356f4b2
7 changed files with 78 additions and 22 deletions
@@ -174,7 +174,10 @@ structure World where
 deriving Inhabited

 instance : ToJson World := ⟨
-  fun world => Json.mkObj [("name", toJson world.name), ("title", world.title)]
+  fun world => Json.mkObj [
+    ("name", toJson world.name),
+    ("title", world.title),
+    ("introduction", world.introduction)]
 ⟩

 /-! ## Game -/