34dc2572f3
This commit fixes issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/deterministic.20timeout/near/287654818 Type class resolution was diverging when trying to synthesize ```lean HSub (optParam Float 0.0) (optParam Float 1.0) ?m.472 ``` and Lean was diverging while unfolding ```lean instance : OfScientific Float where ofScientific m s e := if s then let s := 64 - m.log2 -- ensure we have 64 bits of mantissa left after division let m := (m <<< (3 * e + s)) / 5^e Float.ofBinaryScientific m (-4 * e - s) else Float.ofBinaryScientific (m * 5^e) e ``` was being unfolded. Anothe potential solution for the problem above is to erase the `optParam` annotations before performing type class resolution. |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||