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

fix from lean bump

Browse Source
This commit is contained in:
joneugster
2023-10-18 14:57:14 +02:00
parent ca58cb0e78
commit 2de82a1106
1 changed files with 3 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files
server/GameServer/FileWorker.lean
+3 -3
View File
@@ -65,7 +65,7 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext)
Elab.Command.CommandElabM Unit := do Elab.Command.CommandElabM Unit := do
match stx with match stx with
| .missing => return () | .missing => return ()
| .node info kind args => | .node _info _kind args =>
for arg in args do for arg in args do
findForbiddenTactics inputCtx levelParams arg asError findForbiddenTactics inputCtx levelParams arg asError
| .atom info val => | .atom info val =>
@@ -89,7 +89,7 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext)
| some _ => pure () -- tactic is in the inventory, allow it. | some _ => pure () -- tactic is in the inventory, allow it.
else if tac.disabled then else if tac.disabled then
addWarningMessage info s!"The tactic '{val}' is disabled in this level!" addWarningMessage info s!"The tactic '{val}' is disabled in this level!"
| .ident info rawVal val preresolved => | .ident info _rawVal val _preresolved =>
let ns ← let ns ←
try resolveGlobalConst (mkIdent val) try resolveGlobalConst (mkIdent val)
catch | _ => pure [] -- catch "unknown constant" error catch | _ => pure [] -- catch "unknown constant" error
@@ -395,7 +395,7 @@ section Initialization
-- Set the search path -- Set the search path
Lean.searchPathRef.set paths Lean.searchPathRef.set paths
let env ← importModules [{ module := `Init : Import }, { module := levelParams.levelModule : Import }] {} 0 let env ← importModules #[{ module := `Init : Import }, { module := levelParams.levelModule : Import }] {} 0
-- return (env, paths) -- return (env, paths)
-- use empty header -- use empty header