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