feat: add ImportM.runCoreM

This commit is contained in:
Leonardo de Moura 2022-09-23 07:52:13 -07:00
parent e53ac503da
commit c165317b28

View file

@ -317,4 +317,9 @@ def addAndCompile (decl : Declaration) : CoreM Unit := do
addDecl decl;
compileDecl decl
def ImportM.runCoreM (x : CoreM α) : ImportM α := do
let ctx ← read
let (a, _) ← x.toIO { options := ctx.opts, fileName := "<ImportM>", fileMap := default } { env := ctx.env }
return a
end Lean