Merge pull request #43 from leanprover-community/jmc-unusedtransitive…

…main

chore: move `Core.withImportModules` to `Imports.lean`

ImportGraph.lean

@@ -3,4 +3,3 @@ import ImportGraph.Imports
 import ImportGraph.CurrentModule
 import ImportGraph.Lean.Name
 import ImportGraph.RequiredModules
-import ImportGraph.UnusedTransitiveImports

ImportGraph/Imports.lean

@@ -185,6 +185,12 @@ def unusedTransitiveImports (amongst : List Name) (verbose : Bool := false) : Co
     let unused := (transitiveImports.find? n).getD {} \ (transitivelyRequired.find? n |>.getD {})
     amongst.filter (fun m => unused.contains m))
 
+def Core.withImportModules (modules : Array Name) {α} (f : CoreM α) : IO α := do
+  searchPathRef.set compile_time_search_path%
+  unsafe Lean.withImportModules (modules.map (fun m => {module := m})) {} (trustLevel := 1024)
+    fun env => Prod.fst <$> Core.CoreM.toIO
+        (ctx := { fileName := "<CoreM>", fileMap := default }) (s := { env := env }) do f
+
 /--
 Return the redundant imports (i.e. those transitively implied by another import)
 of a specified module (or the current module if `none` is specified).

ImportGraph/UnusedTransitiveImports.lean

@@ -2,12 +2,6 @@ import ImportGraph.Imports
 
 open Lean
 
-def Core.withImportModules (modules : Array Name) {α} (f : CoreM α) : IO α := do
-  searchPathRef.set compile_time_search_path%
-  unsafe Lean.withImportModules (modules.map (fun m => {module := m})) {} (trustLevel := 1024)
-    fun env => Prod.fst <$> Core.CoreM.toIO
-        (ctx := { fileName := "<CoreM>", fileMap := default }) (s := { env := env }) do f
-
 /--
 `lake exe unused_transitive_imports m1 m2 ...`