From c679325c46d2c721a485d73a59ea621efd405869 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 3 Mar 2023 11:22:58 +0100 Subject: [PATCH] exclude 'only' keyword from forbidden tactics --- server/leanserver/GameServer/FileWorker.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/server/leanserver/GameServer/FileWorker.lean b/server/leanserver/GameServer/FileWorker.lean index 3e3cd1e..f5f2673 100644 --- a/server/leanserver/GameServer/FileWorker.lean +++ b/server/leanserver/GameServer/FileWorker.lean @@ -75,7 +75,7 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) (levelParams : | .atom info val => -- ignore syntax elements that do not start with a letter -- and ignore "with" keyword - if 0 < val.length ∧ val.data[0]!.isAlpha ∧ val != "with" ∧ val != "at" then + if 0 < val.length ∧ val.data[0]!.isAlpha ∧ val != "with" ∧ val != "at" ^ val != "only" then let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp` match levelParams.tactics.find? (fun t => t.name.toString == val) with | none => addErrorMessage info s!"You have not unlocked the tactic '{val}' yet!"