From b9112bfb097ba587d3139c4809be3a8d75c8bb86 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Fri, 3 May 2024 15:16:19 +0200
Subject: [PATCH] add 'using' as known keyword

---
 server/GameServer/Commands.lean      |  2 +-
 server/GameServer/EnvExtensions.lean | 10 +++++++++-
 2 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean
index c2ba0a0..ba3c32a 100644
--- a/server/GameServer/Commands.lean
+++ b/server/GameServer/Commands.lean
@@ -389,7 +389,7 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
     ("level" ++ toString lvlIdx : String)
 
   -- Collect all used tactics/lemmas in the sample proof:
-  let usedInventory ← match val with
+  let usedInventory : UsedInventory ← match val with
   | `(Parser.Command.declVal| := $proof:term) => do
     collectUsedInventory proof
   | _ => throwError "expected `:=`"
diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean
index d2b86c4..cab6d1e 100644
--- a/server/GameServer/EnvExtensions.lean
+++ b/server/GameServer/EnvExtensions.lean
@@ -12,7 +12,7 @@ Note: Added `clear` tactic because currently it is very useful in combination wi
 hypotheses).
 -/
 def GameServer.ALLOWED_KEYWORDS : List String :=
-  ["with", "fun", "at", "only", "by", "generalizing", "if", "then", "else", "clear"]
+  ["with", "fun", "at", "only", "by", "generalizing", "if", "then", "else", "clear", "using"]
 
 /-- The default game name if `Game "MyGame"` is not used. -/
 def defaultGameName: String := "MyGame"
@@ -532,3 +532,11 @@ def modifyLevel (levelId : LevelId) (fn : GameLevel → m GameLevel) [MonadError
   let world' := {world with levels := world.levels.insert levelId.level level'}
   let game' := {game with worlds := game.worlds.insertNode levelId.world world'}
   insertGame levelId.game game'
+
+-- def getIntroducedInventory (game : Game) [MonadError m] : m (Array Name) := do
+--   let allItems : Array Name := game.worlds.nodes.fold (fun L _ world => L ++
+--     world.levels.fold (fun LL _ level =>
+--       LL ++ level.tactics.new ++ level.lemmas.new
+--     ) #[]) #[]
+
+--   pure allItems