phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

exclude 'only' keyword from forbidden tactics

Browse Source
This commit is contained in:
Jon Eugster
2023-03-03 11:22:58 +01:00
parent c015d1e1f9
commit c679325c46
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
server/leanserver/GameServer/FileWorker.lean
+1 -1
View File
@@ -75,7 +75,7 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) (levelParams :
| .atom info val => | .atom info val =>
-- ignore syntax elements that do not start with a letter -- ignore syntax elements that do not start with a letter
-- and ignore "with" keyword -- 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` 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 match levelParams.tactics.find? (fun t => t.name.toString == val) with
| none => addErrorMessage info s!"You have not unlocked the tactic '{val}' yet!" | none => addErrorMessage info s!"You have not unlocked the tactic '{val}' yet!"