From e3c14256fbcb548dedd5800815e4c9a1c6098b8e Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Fri, 28 Apr 2023 12:43:10 +0200
Subject: [PATCH] revert attributes for statements

---
 server/GameServer/Commands.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean
index 5b94ff9..228a81b 100644
--- a/server/GameServer/Commands.lean
+++ b/server/GameServer/Commands.lean
@@ -224,9 +224,10 @@ def reprint (stx : Syntax) : Format :=
 
 /-- A `attr := ...` option for `Statement`. Add attributes to the defined theorem. -/
 syntax statementAttr := "(" &"attr" ":=" Parser.Term.attrInstance,* ")"
+-- TODO
 
 /-- Define the statement of the current level. -/
-elab "Statement" statementName:ident ? attr:statementAttr ? descr:str ? sig:declSig val:declVal : command => do
+elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : command => do
   let lvlIdx ← getCurLevelIdx
 
   -- Save the messages before evaluation of the proof.