chore: remove leftover

2026-04-11 22:54:17 +00:00 · 2026-01-04 13:34:32 -08:00
1 changed files with 0 additions and 1 deletions
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -1854,7 +1854,6 @@ end
      failK
  | none   => failK

-set_option trace.Compiler.result true in
 private def isDefEqOnFailure (t s : Expr) : MetaM Bool := do
  withTraceNodeBefore `Meta.isDefEq.onFailure (fun _ => return m!"{t} =?= {s}") do
    unstuckMVar t (fun t => Meta.isExprDefEqAux t s) <|