chore: add matchHEq?

src/Lean/Meta/MatchUtil.lean

@@ -9,7 +9,7 @@ import Lean.Meta.Basic
 namespace Lean.Meta
 
 @[inline] def testHelper (e : Expr) (p : Expr → MetaM Bool) : MetaM Bool := do
-  if (← p e) then 
+  if (← p e) then
     return true
   else
     p (← whnf e)
@@ -19,25 +19,28 @@ namespace Lean.Meta
   | none => p? (← whnf e)
   | s    => return s
 
-def matchEq? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) := 
+def matchEq? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) :=
   matchHelper? e fun e => return Expr.eq? e
 
+def matchHEq? (e : Expr) : MetaM (Option (Expr × Expr × Expr × Expr)) :=
+  matchHelper? e fun e => return Expr.heq? e
+
 def matchFalse (e : Expr) : MetaM Bool := do
   testHelper e fun e => return e.isConstOf ``False
 
-def matchNot? (e : Expr) : MetaM (Option Expr) := 
-  matchHelper? e fun e => do 
+def matchNot? (e : Expr) : MetaM (Option Expr) :=
+  matchHelper? e fun e => do
     if let some e := e.not? then
       return e
     else if let some (a, b) := e.arrow? then
       if (← matchFalse b) then return some a else return none
-    else  
-      return none 
+    else
+      return none
 
 def matchNe? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) :=
   matchHelper? e fun e => do
     if let some r := e.ne? then
-      return r  
+      return r
     else if let some e ← matchNot? e then
       matchEq? e
     else
@@ -45,7 +48,7 @@ def matchNe? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) :=
 
 def matchConstructorApp? (e : Expr) : MetaM (Option ConstructorVal) := do
   let env ← getEnv
-  matchHelper? e fun e => 
+  matchHelper? e fun e =>
     return e.isConstructorApp? env
 
 end Lean.Meta