Additional functions using CoreM state.

def CoreM.withImportModules {α : Type} (modules : Array Lean.Name) (run : Lean.CoreM α) (searchPath : Option Lean.SearchPath := none) (options : Lean.Options := ∅) (trustLevel : UInt32 := 0) (fileName : String := "") : IO α

Run a CoreM α in a fresh Environment with specified modules : List Name imported.

Equations

• CoreM.withImportModules modules run searchPath options trustLevel fileName = CoreM.withImportModules.unsafe_impl_5✝ modules run searchPath options trustLevel fileName