Additional functions using CoreM state. #
def
CoreM.withImportModules
{α : Type}
(modules : Array Lean.Name)
(run : Lean.CoreM α)
(searchPath : Option Lean.SearchPath := none)
(options : Lean.Options := { entries := [] })
(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_1 modules run searchPath options trustLevel fileName