max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: typo

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-10 08:36:48 -08:00
parent 27158eb3e2
commit d7b23cf297
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Meta/SynthInstance.lean
View file

@ -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