chore: add forEachEqc

leanprover · Dec 24, 2024 · 6b8caf7 · 6b8caf7
1 parent ec80de2
commit 6b8caf7
Showing 1 changed file with 6 additions and 0 deletions.
diff --git 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