Zulip Chat Archive

Stream: PR reviews

Topic: lean#282 changing structure instance elaboration


view this post on Zulip Gabriel Ebner (May 28 2020 at 14:02):

This is a somewhat large and fundamental change, but it fixes two bugs (I can't tell whether the bugs are annoying or not). There are some changes to mathlib necessary: https://github.com/leanprover-community/mathlib/compare/si

view this post on Zulip Scott Morrison (May 28 2020 at 14:09):

Thank you so much for tracking down all the problems in mathlib!

view this post on Zulip Scott Morrison (May 28 2020 at 14:09):

I would really love to see these bugs in Lean fixed.

view this post on Zulip Scott Morrison (May 28 2020 at 14:09):

And that level of changes required in mathlib seems like a small price to pay.

view this post on Zulip Scott Morrison (May 28 2020 at 14:11):

Hopefully some of the mathlib changes can still be cleaned up or refactored further. I won't have a chance tomorrow, but I'd be very happy to see this as part of the Lean 3.15 PR. :-)

view this post on Zulip Kevin Buzzard (May 28 2020 at 14:26):

I too would love to see these bugs fixed. Having \in randomly unfolding to set.mem confuses newcomers.

view this post on Zulip Gabriel Ebner (May 28 2020 at 15:02):

Ok, then it is decided.


Last updated: May 06 2021 at 11:23 UTC