## Stream: PR reviews

### Topic: lean#282 changing structure instance elaboration

#### 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

#### Scott Morrison (May 28 2020 at 14:09):

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

#### Scott Morrison (May 28 2020 at 14:09):

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

#### Scott Morrison (May 28 2020 at 14:09):

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

#### 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. :-)

#### 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.

#### Gabriel Ebner (May 28 2020 at 15:02):

Ok, then it is decided.

Last updated: May 06 2021 at 11:23 UTC