diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean index fd1044c..fee9758 100644 --- a/server/leanserver/GameServer/Commands.lean +++ b/server/leanserver/GameServer/Commands.lean @@ -62,7 +62,7 @@ partial def reprintCore : Syntax → Option Format def reprint (stx : Syntax) : Format := reprintCore stx |>.getD "" -syntax hintArg := " (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")" +syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")") /-- A tactic that can be used inside `Statement`s to indicate in which proof states players should see hints. The tactic does not affect the goal state. -/