diff --git a/src/Lean/Compiler/LCNF/PhaseExt.lean b/src/Lean/Compiler/LCNF/PhaseExt.lean index 3f9bfc737e..daa6964918 100644 --- a/src/Lean/Compiler/LCNF/PhaseExt.lean +++ b/src/Lean/Compiler/LCNF/PhaseExt.lean @@ -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 \ No newline at end of file