From 9ef4122e944bc90959c075fa48ab608cce159211 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sun, 6 Aug 2023 23:52:11 +0200 Subject: [PATCH] add allowed keywords 'by' and 'to' --- server/GameServer/FileWorker.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index 7af7911..979533d 100644 --- a/server/GameServer/FileWorker.lean +++ b/server/GameServer/FileWorker.lean @@ -71,7 +71,7 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) | .atom info val => -- ignore syntax elements that do not start with a letter -- and ignore "with" keyword - let allowed := ["with", "fun", "at", "only"] + let allowed := ["with", "fun", "at", "only", "by", "to"] if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp` match levelParams.tactics.find? (·.name.toString == val) with