fixes of lean bump

2023-10-19 12:10:58 +02:00
parent 2de82a1106
commit 5de8ce8be7
2 changed files with 5 additions and 2 deletions
@@ -91,7 +91,7 @@ def createEnv (gameDir : String) (module : String) : IO Environment := do
  -- Set the search path
  Lean.searchPathRef.set paths

-  let env ← importModules [{ module := `Init : Import }, { module := module : Import }] {} 0
+  let env ← importModules #[{ module := `Init : Import }, { module := module : Import }] {} 0
  return env

 def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do