uniformize binders

Stream: mathlib4

[Floris van Doorn]

Can we uniformize what binder notation is allowed?

import Mathlib.Order.SetNotation

#check ∃ n : ℕ, n = n
#check ∃ (n : ℕ), n = n
#check ∃ n m : ℕ, n = n
#check ∃ (n m : ℕ), n = n
#check ∃ n < 5, n = n
#check ∃ (n < 5), n = n -- error
#check ⋃ n : ℕ, {n}
#check ⋃ (n : ℕ), {n}
#check ⋃ n m : ℕ, {n} -- error
#check ⋃ (n m : ℕ), {n} -- error
#check ⋃ n < 5, {n}
#check ⋃ (n < 5), {n}

[Floris van Doorn]

(@Kyle Miller)

[Eric Wieser]

This gets even more complex with the finset summation notation, for which only some binders make sense

[Yaël Dillies]

(please don't bring up ∑ _, _ and {_ | _} :see_no_evil:)

[Yaël Dillies]

(too late :grinning:)