fix termlikedefeq issue

leanprover-community · Jan 13, 2025 · 57c655e · 57c655e
1 parent 12b16cc
commit 57c655e
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/Auto/Translation/Monomorphization.lean b/Auto/Translation/Monomorphization.lean
@@ -620,12 +620,15 @@ def termLikeDefEqDefEqs (lemmas : Array Lemma) : MetaM (Array Lemma) := do
         if let .ok (.some (proof, eq, params)) ← computation then
           let eq := Expr.eraseMData (← Core.betaReduce eq)
           let eq ← Meta.transform eq (pre := fun e => do return .continue (← unfoldProj e))
-          let_expr Eq _ lhs rhs := eq | continue
-          if lhs == rhs then
+          if ← isTrivialEq eq then
             continue
           trace[auto.mono.termLikeDefEq] "{eq}"
           ret := ret.push ⟨⟨proof, eq, .leaf "termLikeDefEq"⟩, params⟩
   return ret
+where
+  isTrivialEq (e : Expr) : MetaM Bool := Meta.forallTelescope e fun _ b => do
+    let_expr Eq _ lhs rhs := b | return false
+    return lhs == rhs
 
 def initializeMonoM (lemmas : Array Lemma) : MonoM Unit := do
   let lemmas := lemmas ++ (← termLikeDefEqDefEqs lemmas)