Zulip Chat Archive

Stream: general

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: Dec 20 2023 at 11:08 UTC