fix

leanprover-community · Dec 9, 2024 · 24fd40e · 24fd40e
1 parent 73e5d9d
commit 24fd40e
Showing 1 changed file with 6 additions and 5 deletions.
diff --git a/Mathlib/Lean/CoreM.lean b/Mathlib/Lean/CoreM.lean
@@ -19,8 +19,9 @@ def CoreM.withImportModules {α : Type} (modules : Array Name) (run : CoreM α)
     (trustLevel : UInt32 := 0) (fileName := "") :
     IO α := unsafe do
   if let some sp := searchPath then searchPathRef.set sp
-  Lean.withImportModules (trustLevel := trustLevel) (modules.map (Import.mk · false)) options fun env =>
-    let ctx := {fileName, options, fileMap := default}
-    let state := {env}
-    Prod.fst <$> (CoreM.toIO · ctx state) do
-      run
+  Lean.withImportModules (trustLevel := trustLevel) (modules.map (Import.mk · false)) options
+    fun env =>
+      let ctx := {fileName, options, fileMap := default}
+      let state := {env}
+      Prod.fst <$> (CoreM.toIO · ctx state) do
+        run