From 65ed45fe16c58b98519d6947f513cc8bc23e289e Mon Sep 17 00:00:00 2001
From: "Alex J. Best" <alex.j.best@gmail.com>
Date: Fri, 4 Aug 2023 16:56:36 +0100
Subject: [PATCH 1/2] add attributes

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

diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean
index 455b8a8..40a18c9 100644
--- a/server/GameServer/Commands.lean
+++ b/server/GameServer/Commands.lean
@@ -283,7 +283,7 @@ syntax statementAttr := "(" &"attr" ":=" Parser.Term.attrInstance,* ")"
 -- TODO
 
 /-- Define the statement of the current level. -/
-elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : command => do
+elab attrs:Lean.Parser.Term.attributes ? "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : command => do
   let lvlIdx ← getCurLevelIdx
 
   let descr := match descr with
@@ -298,6 +298,7 @@ elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : com
   let defaultDeclName : Ident := mkIdent <| (← getCurGame).name ++ (← getCurWorld).name ++
     ("level" ++ toString lvlIdx : String)
 
+  let doc? : Option (TSyntax ``Parser.Command.docComment) := none
   -- Add theorem to context.
   match statementName with
   | some name =>
@@ -311,19 +312,19 @@ elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : com
       -- in that case.
       logWarningAt name (m!"Environment already contains {fullName}! Only the existing " ++
       m!"statement will be available in later levels:\n\n{origType}")
-      let thmStatement ← `(theorem $defaultDeclName $sig $val)
+      let thmStatement ← `(command| $[$doc?]? $[$attrs]? theorem $defaultDeclName $sig $val)
       elabCommand thmStatement
       -- Check that statement has a docs entry.
       checkInventoryDoc .Lemma name (template := descr)
 
     else
-      let thmStatement ← `( theorem $name $sig $val)
+      let thmStatement ← `(command| $[$doc?]? $[$attrs]? theorem $name $sig $val)
       elabCommand thmStatement
       -- Check that statement has a docs entry.
       checkInventoryDoc .Lemma name (template := descr)
 
   | none =>
-    let thmStatement ← `(theorem $defaultDeclName $sig $val)
+    let thmStatement ← `(command| $[$doc?]? $[$attrs]? theorem $defaultDeclName $sig $val)
     elabCommand thmStatement
 
   let msgs := (← get).messages

From 88e9ee7155311799eedc3e6dfbca2ce0b1012516 Mon Sep 17 00:00:00 2001
From: "Alex J. Best" <alex.j.best@gmail.com>
Date: Fri, 4 Aug 2023 17:56:16 +0100
Subject: [PATCH 2/2] better

---
 server/GameServer/Commands.lean | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean
index 40a18c9..ca7a585 100644
--- a/server/GameServer/Commands.lean
+++ b/server/GameServer/Commands.lean
@@ -298,7 +298,6 @@ elab attrs:Lean.Parser.Term.attributes ? "Statement" statementName:ident ? descr
   let defaultDeclName : Ident := mkIdent <| (← getCurGame).name ++ (← getCurWorld).name ++
     ("level" ++ toString lvlIdx : String)
 
-  let doc? : Option (TSyntax ``Parser.Command.docComment) := none
   -- Add theorem to context.
   match statementName with
   | some name =>
@@ -312,19 +311,19 @@ elab attrs:Lean.Parser.Term.attributes ? "Statement" statementName:ident ? descr
       -- in that case.
       logWarningAt name (m!"Environment already contains {fullName}! Only the existing " ++
       m!"statement will be available in later levels:\n\n{origType}")
-      let thmStatement ← `(command| $[$doc?]? $[$attrs]? theorem $defaultDeclName $sig $val)
+      let thmStatement ← `(command| $[$attrs:attributes]? theorem $defaultDeclName $sig $val)
       elabCommand thmStatement
       -- Check that statement has a docs entry.
       checkInventoryDoc .Lemma name (template := descr)
 
     else
-      let thmStatement ← `(command| $[$doc?]? $[$attrs]? theorem $name $sig $val)
+      let thmStatement ← `(command| $[$attrs:attributes]? theorem $name $sig $val)
       elabCommand thmStatement
       -- Check that statement has a docs entry.
       checkInventoryDoc .Lemma name (template := descr)
 
   | none =>
-    let thmStatement ← `(command| $[$doc?]? $[$attrs]? theorem $defaultDeclName $sig $val)
+    let thmStatement ← `(command| $[$attrs:attributes]? theorem $defaultDeclName $sig $val)
     elabCommand thmStatement
 
   let msgs := (← get).messages