Postfix operator precendence issue

Stream: lean4

[Sebastian Reichelt]

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?

[Mario Carneiro]

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

[Mario Carneiro]

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)

[Sebastian Ullrich]

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