From a969014eb9b1d5d4db1e3151c083ed3e3afe470b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 25 Jan 2022 18:20:06 -0800
Subject: [PATCH] chore: add `matchHEq?`

---
 src/Lean/Meta/MatchUtil.lean | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

diff --git a/src/Lean/Meta/MatchUtil.lean b/src/Lean/Meta/MatchUtil.lean
index 1f1ff7dea3..6e22f2913b 100644
--- a/src/Lean/Meta/MatchUtil.lean
+++ b/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