Zulip Chat Archive

Stream: general

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 dselsam:fix-tc-loop...

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: Dec 20 2023 at 11:08 UTC