From 86302522a54eb01b8d407aea571ebc0c15667122 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Wed, 15 Mar 2023 17:02:43 +0100 Subject: [PATCH] add atomic to fix interpolatedStr issue --- server/leanserver/GameServer/Commands.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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. -/