From c2b298e6507847850be5215981b9b4b12741ff53 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Mon, 3 Apr 2023 11:53:10 +0200
Subject: [PATCH] fix

---
 server/leanserver/GameServer/Commands.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean
index df8db18..3fc828e 100644
--- a/server/leanserver/GameServer/Commands.lean
+++ b/server/leanserver/GameServer/Commands.lean
@@ -326,6 +326,11 @@ Arguments:
 -/
 elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : command => do
 
+  -- Check that the statement name is a lemma in the doc
+  match statementName with
+  | some name => checkInventoryDoc .Lemma name.getId
+  | none => pure Unit.unit
+
   let lvlIdx ← getCurLevelIdx
   let defaultDeclName : Name := (← getCurGame).name ++ (← getCurWorld).name ++
     ("level" ++ toString lvlIdx : String)