issue !4#5127: `∃ x ∈ s, P x` parses differently

Stream: triage

[Random Issue Bot]

Today I chose issue 5127 for discussion!

∃ x ∈ s, P x parses differently
Created by @Ruben Van de Velde (@Ruben-VandeVelde) on 2023-06-16
Labels: lean4-change-in-behaviour

Is this issue still relevant? Any recent updates? Anyone making progress?

[Anatole Dedecker]

I think this is no longer an issue and all the library made the switch ?

[Yaël Dillies]

Not quite all the library. Look for "expanded binder collection" in mathport comments.