diff --git a/src/Init/Lean/Meta/SynthInstance.lean b/src/Init/Lean/Meta/SynthInstance.lean index 29920bc05e..8d7b92926c 100644 --- a/src/Init/Lean/Meta/SynthInstance.lean +++ b/src/Init/Lean/Meta/SynthInstance.lean @@ -324,7 +324,7 @@ def wakeUp (answer : Answer) : Waiter → SynthM Unit def isNewAnswer (oldAnswers : Array Answer) (answer : Answer) : Bool := oldAnswers.all $ fun oldAnswer => do - -- Remark: isDefEq here is too expensive. TODO: if `==` is to imprecise, add some light normalization to `resultType` at `addAnswer` + -- Remark: isDefEq here is too expensive. TODO: if `==` is too imprecise, add some light normalization to `resultType` at `addAnswer` -- iseq ← isDefEq oldAnswer.resultType answer.resultType; pure (!iseq) oldAnswer.resultType != answer.resultType