Zulip Chat Archive
Stream: triage
Topic: issue !4#5127: `∃ x ∈ s, P x` parses differently
Random Issue Bot (Feb 27 2024 at 14:06):
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 (Feb 28 2024 at 18:06):
I think this is no longer an issue and all the library made the switch ?
Yaël Dillies (Feb 28 2024 at 18:28):
Not quite all the library. Look for "expanded binder collection" in mathport comments.
Random Issue Bot (Oct 10 2025 at 14:12):
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?
Ruben Van de Velde (Oct 10 2025 at 14:24):
I think Yaël's assessment upthread is still accurate
Random Issue Bot (Nov 13 2025 at 14:12):
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?
Last updated: Dec 20 2025 at 21:32 UTC