mark inventory item from the last level

server/GameServer/Commands.lean

@@ -973,6 +973,10 @@ elab "MakeGame" : command => do
               name := name
               displayName := data.displayName
               category := data.category
+              world := worldId
+              -- from the previous level. This is fine b/c in practise levels start at 1
+              level := (levelId - 1 : Nat)
+              proven := true
               altTitle := data.statement
               locked := false }
 

server/GameServer/EnvExtensions.lean

@@ -93,6 +93,12 @@ structure InventoryTile where
   displayName : String
   /-- Category to group inventory items by (currently only used for lemmas). -/
   category : String
+  /-- The world which introduced this item. -/
+  world : Option Name := none
+  /-- The level which introduced this item. -/
+  level : Option Nat := none
+  /-- Set to `true` if there exists an exercise in the game proving this statement. -/
+  proven := false
   /-- If `true` then the item only gets unlocked in a later level. -/
   locked := true
   /-- If `true` then the item is blocked for this level. -/