Parenthesization in docs

Stream: general

[Kyle Miller]

There seems to be some oddness in parenthesization in the docs vs the pretty printer. For docs#real.rpow_mul, within Lean it shows x ^ (y * z) = (x ^ y) ^ z, but the docs show x ^ y * z = (x ^ y) ^ z, which is not correct. For docs#real.mul_self_sqrt, within Lean it shows real.sqrt x * real.sqrt x = x, but the docs show (real.sqrt x) * real.sqrt x = x, which is ok but strange. Is this a known problem?

[Yaël Dillies]

Are there locales changing notation precedence?

[Reid Barton]

I mentioned the ^ one here a little while back and the * is probably for the same reason, hang on...

[Reid Barton]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/pow.2Fmul.20associativity/near/264683881

[Mario Carneiro]

Uh, that should be an error. Tokens should never have more than one precedence