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):

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

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