Topic: Lean 4 tc order
Patrick Massot (Apr 01 2020 at 09:01):
@Daniel Selsam could you comment on https://github.com/leanprover/lean4/pull/130/? I thought the Lean 4 TC system was avoiding every loop problem.
Mario Carneiro (Apr 01 2020 at 09:07):
It might not be a loop problem. We do that in mathlib to put the fast fail typeclasses before the ones with many instances
Patrick Massot (Apr 01 2020 at 09:13):
The name of the branch is
Patrick Massot (Apr 01 2020 at 09:14):
And even with Mario's explanation, I kind of hoped that all the tc subtleties without any mathematical content would be gone in Lean 4.
Daniel Selsam (Apr 01 2020 at 13:34):
@Patrick Massot I have been using the old frontend with the old typeclass resolution procedure. The new frontend is still missing a few necessary features, e.g. an equation compiler. The fix is only relevant for using the old procedure.
Patrick Massot (Apr 01 2020 at 13:36):
Last updated: May 12 2021 at 05:19 UTC