From 02db8617f6b00c5bb7cef2b96d9d08d1331ea2e8 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 3 Mar 2023 12:07:22 +0100 Subject: [PATCH] add 'fun' keyword to allowed tactics --- server/leanserver/GameServer/FileWorker.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/server/leanserver/GameServer/FileWorker.lean b/server/leanserver/GameServer/FileWorker.lean index f5f2673..3326fa8 100644 --- a/server/leanserver/GameServer/FileWorker.lean +++ b/server/leanserver/GameServer/FileWorker.lean @@ -65,8 +65,9 @@ section Elab -- TODO: use HashSet for allowed tactics? /-- Find all tactics in syntax object that are forbidden according to a set `allowed` of allowed tactics. -/ -partial def findForbiddenTactics (inputCtx : Parser.InputContext) (levelParams : Game.DidOpenLevelParams) (stx : Syntax) - : Elab.Command.CommandElabM Unit := do +partial def findForbiddenTactics (inputCtx : Parser.InputContext) + (levelParams : Game.DidOpenLevelParams) (stx : Syntax) : + Elab.Command.CommandElabM Unit := do match stx with | .missing => return () | .node info kind args => @@ -75,7 +76,8 @@ 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" ^ val != "only" then + let allowed := ["with", "fun", "at", "only"] + 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? (fun t => t.name.toString == val) with | none => addErrorMessage info s!"You have not unlocked the tactic '{val}' yet!"