warning: expanding binder collection

Stream: mathlib4

[Xavier Roblot]

In mathlib#1673, I have a couple of error messages: warning: expanding binder collection (y «expr ∉ » t), however the corresponding lemmas compile fine. What I am supposed to do there? Thus leave the warnings and move on? Delete the warnings and move on? Something else?

[Kevin Buzzard]

Don't delete anything that you don't understand without leaving a porting note :-)

[Patrick Massot]

How far are we from geeting rid of all those ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j)? There are now some of the most ugly remaining porting scars.

[Ruben Van de Velde]

I could remove them now

[Patrick Massot]

Is the reasonnable syntax now supported?

[Ruben Van de Velde]

Oh, I thought it was the comments that bothered you. No, it isn't

[Ruben Van de Velde]

Though it may not be too hard... Let's see how much this breaks

[Ruben Van de Velde]

(Pretty hard if you don't know what you're doing)

[Patrick Massot]

I appreciate that you tried, but I fear this may require a @Mario Carneiro or a @Kyle Miller.

[Kyle Miller]

I took a very brief look, and you need to do things like convert ∀ (a) (_ : a ∉ s), 1 ≤ g a to ∀ a ∉ s, 1 ≤ g a. Parentheses are not allowed for extended binders.

At least some of the warnings, like for docs#Set.iUnion₂_congr, seem to be sort of false alarms, but there are still some parentheses to clean up (⋃ (i) (j), s i j to ⋃ i j, s i j)

[Patrick Massot]

Kyle Miller said:

I took a very brief look, and you need to do things like convert ∀ (a) (_ : a ∉ s), 1 ≤ g a to ∀ a ∉ s, 1 ≤ g a. Parentheses are not allowed for extended binders.

I took care of ∀ a ∉ s recently.

At least some of the warnings, like for docs#Set.iUnion₂_congr, seem to be sort of false alarms, but there are still some parentheses to clean up (⋃ (i) (j), s i j to ⋃ i j, s i j)

Yes, those are the remaining issues.

[Patrick Massot]

⋃ i j, s i j simply doesn't work.

[Kyle Miller]

Oh right, I forgot about this limitation. With the experimental #7227 it would work.

[Patrick Massot]

But it is marked as WIP and doesn't build :sad:

[Patrick Massot]

It seems only tests do not build. Maybe those tests need to be updated?

[Kyle Miller]

I'm still working on it (and the non-building is some tests)

[Eric Wieser]

#7227 has lots of cool stuff, but I'm a bit unhappy about the fact that the ∈ is now being used in a place where it is not literally syntax for Membership.mem, even though morally it sort of is.