JovanGerb
JovanGerb
!bench I now properly did the loop detection. But it should give at most a very small improvement.
!bench I added an `isDefEq` check that is technically necessary (but it not being there didn't cause any problems). Let's see how it affects speed.
!bench I added a check so that the intermediate caching isn't used for `outParam` type classes. Hopefully that doesn't slow it down.
!bench
Can anyone explain why the output on two of the tests doesn't match the expectation? These tests have nothing to do with type classes...
Out of the two errors, the second one has magically disappeared. The remaining error is a reshuffling of error messages (it doesn't look like one order is more correct than...
How do I interpret the benchmark results? I just see a huge wall of numbers when clicking on the link. I suppose we are most interested in mathlib times? which...
I've made a draft PR that fixes the bad example: #4223
Orthogonal to the fix in #5291 (which is the fix as described in this RFC), we can still set a low priority for `Lean.MonadError.toMonadExceptOf`, `Lean.MonadError.toMonadRef` and `Lean.MonadError.toAddErrorMessageContext`, which, as seen...