feat: add forEachDecl for LCNF

This commit is contained in:
Leonardo de Moura 2022-09-24 20:18:27 -07:00
parent cf2b6b80bb
commit afb457ca2a

View file

@ -54,4 +54,11 @@ def getDecl? (declName : Name) : CompilerM (Option Decl) := do
def saveBase : Pass :=
.mkPerDeclaration `saveBase (fun decl => do decl.saveBase; return decl) .base
def forEachDecl (f : Decl → CoreM Unit) : CoreM Unit := do
let env ← getEnv
for modIdx in [:env.allImportedModuleNames.size] do
for decl in baseExt.getModuleEntries env modIdx do
f decl
baseExt.getState env |>.forM fun _ decl => f decl
end Lean.Compiler.LCNF