Zulip Chat Archive

Stream: general

Topic: Lean 4 tc order


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 01 2020 at 09:13):

The name of the branch is dselsam:fix-tc-loop...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Apr 01 2020 at 13:36):

Thanks!


Last updated: May 12 2021 at 05:19 UTC