From afb457ca2aec8be1631980e3979a37258d822d70 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 24 Sep 2022 20:18:27 -0700
Subject: [PATCH] feat: add `forEachDecl` for LCNF

---
 src/Lean/Compiler/LCNF/PhaseExt.lean | 7 +++++++
 1 file changed, 7 insertions(+)

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