From 6b8caf7e500ba065e7521e0784866841ca397775 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 24 Dec 2024 15:19:48 -0800
Subject: [PATCH] chore: add `forEachEqc`

---
 src/Lean/Meta/Tactic/Grind/Types.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index e4d85786a4..c505b4ce6f 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -429,4 +429,10 @@ def filterENodes (p : ENode → GoalM Bool) : GoalM (Array ENode) := do
       ref.modify (·.push n)
   ref.get
 
+def forEachEqc (f : ENode → GoalM Unit) : GoalM Unit := do
+  let nodes ← getENodes
+  for n in nodes do
+    if isSameExpr n.self n.root then
+      f n
+
 end Lean.Meta.Grind