Question about notation: bound variable after an expression

Stream: mathlib4

[Yury G. Kudryashov]

I'm not sure yet if this would be a good change or not, but I wonder if Lean 4 allows us to change notation like f ≤ᶠ[l] g to something like f x ≤ᶠ[x ∈ l] g x. It may be more convenient if f, g, or both of them are already in the form of fun x => expr, especially in calc blocks. Similarly, can we move x in the notation for integrals to the end like we write in informal texts? AFAIR, the main reason for having it before the expression in Lean 3 was technical difficulty of writing the parser.

[Kenny Lau]

I think my experiments with limit notation show that it is possible to put the function variable afterwards

[Yury G. Kudryashov]

I'm not sure yet that we want it, so please don't spend your time on implementing the change.

[Kenny Lau]

I'm not sure a lot needs to be changed anyway, but from the previous limit notation discussion there might be concerns about implicitly requiring every function to be eta-expanded?

[Yury G. Kudryashov]

I guess, this is the main concern.