Postfix operator precedence issue

Stream: lean4

[Sebastian Reichelt]

Thanks, that clears it up.
@Mario Carneiro I hadn't realized this, but it seems that since March 23 the operator definition is simply ignored if a precedence higher than 1024 is specified.

[Sebastian Ullrich]

As written in https://leanprover.github.io/lean4/doc/syntax.html#notations-and-precedence,

postfix:1025 "⁻¹"  => Inv.inv

is (now) expanded to

notation:1025 arg:1025 "⁻¹" => Inv.inv arg

Since there is no other notation at this level, arg cannot be filled, yes. I'm not sure there is a practical reason to ever go over max.

[Mario Carneiro]

I'm not sure there is a practical reason to ever go over max.

I think the name max is a misnomer here. The precedence of application is 1024, which is by no means (should not be) the highest precedence. Why? Because you might want things that bind tighter than application, like these postfix operator examples. max should be something like 2048 at least and let the precedence of application stay at 1024.

[Mario Carneiro]

The only things that should have "max precedence" are parentheses and atoms