Topic: Parenthesization in docs
Kyle Miller (Feb 03 2022 at 03:25):
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 (Feb 03 2022 at 08:16):
Are there locales changing notation precedence?
Reid Barton (Feb 03 2022 at 08:21):
I mentioned the
^ one here a little while back and the
* is probably for the same reason, hang on...
Reid Barton (Feb 03 2022 at 08:22):
Mario Carneiro (Feb 03 2022 at 08:27):
Uh, that should be an error. Tokens should never have more than one precedence
Last updated: Aug 03 2023 at 10:10 UTC