From 57c655ee583c735ed9219e9277382e9876dd6e21 Mon Sep 17 00:00:00 2001 From: PratherConid Date: Sun, 12 Jan 2025 17:34:36 -0800 Subject: [PATCH] fix termlikedefeq issue --- Auto/Translation/Monomorphization.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Auto/Translation/Monomorphization.lean b/Auto/Translation/Monomorphization.lean index fe47a0e..9d0e69b 100644 --- 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)