Binding power of `^ [n]`

Stream: general

[Sebastien Gouezel]

Some time ago, we noticed that - 2 ^ 3 was parsed as (-2)^3, and we fixed the priority of ^ to make it more reasonable. I was just bitten by the same issue but for iterates of a map: - f^[n] 0, which for me means - (f^[n] 0), is parsed as (-f)^[n] 0 (I am in a context where -fmakes sense). Is there a way to fix this in the same way it was done for powers? (Unfortunately for me, the notation is declared in core...)

[Yury G. Kudryashov]

And while we're at it, what about fixing binding power of supr/Union/infi/Inter so that it doesn't eat = in ⋃ i, s i = t?

[Patrick Massot]

Oh yes, that would be so nice!

[Eric Wieser]

Are those notations in core, @Yury G. Kudryashov?

[Eric Wieser]

I thought those were mathlib, making them much easier to fix than src#nat.iterate

[Yury G. Kudryashov]

sUnion is in the core (BTW, should we move it to mathlib?)

[Kevin Buzzard]

if we're complaining about standard notation, can I add to the list the fact that \union and \inter are left associative, whereas \and and \or are right associative.

[Yury G. Kudryashov]

The rest is in mathlib

[Yury G. Kudryashov]

@Kevin Buzzard Changing associativity means that lots of code will break.

[Kevin Buzzard]

I was just surprised about the asymmetry

[Sebastien Gouezel]

Did you know that, currently, (1 / (n : ℝ)) • f^[n] 0 is parsed as ((1 / (n : ℝ)) • f)^[n] 0? You can guess it took me some time to figure out what was going on :-)

[Yury G. Kudryashov]

^[n] eats a lot on the LHS. I don't remember if it eats =.