Zulip Chat Archive

Stream: lean4

Topic: Postfix operator precendence issue

view this post on Zulip Sebastian Reichelt (Apr 06 2021 at 20:32):

I'd like to report a minor issue with operator levels that I ran into when upgrading from nightly build 2021-03-22 to 2021-03-23 -- or maybe it's just a documentation problem. I define a postfix ⁻¹ operator as described in syntax.md, but I had to increase its level to at least 1024 so I could use it in function arguments without superfluous parentheses. Up to 2021-03-22, this worked with all levels >= 1024, but since 2021-03-23, only 1023 and 1024 work; otherwise it binds too strongly. In any case, 1000 is too weak, and I'm a bit concerned that max is actually defined to be 1000. Am I missing something?

view this post on Zulip Mario Carneiro (Apr 07 2021 at 00:11):

Do you have examples where the binding is "too strong" and what you expect?

view this post on Zulip Mario Carneiro (Apr 07 2021 at 00:13):

The precendence of application is 1024, which explains why it would be relevant here. For example, f x⁻¹ is interpreted as (f x)⁻¹ if the precedence is less than 1024 and f (x⁻¹) if it is higher than 1024. (If it is equal then I guess it depends on whether it is left- or right-associative, and I doubt this is what you want in any case)

view this post on Zulip Sebastian Ullrich (Apr 07 2021 at 07:20):

max is 1024. 1000 was a typo in syntax.md.

Last updated: May 07 2021 at 12:15 UTC