## Stream: lean4

### Topic: Postfix operator precedence issue

#### Sebastian Reichelt (Apr 07 2021 at 20:25):

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 (Apr 07 2021 at 20:54):

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 (Apr 07 2021 at 21:35):

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 (Apr 07 2021 at 21:36):

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

Last updated: May 18 2021 at 22:15 UTC