Zulip Chat Archive

Stream: lean4

Topic: Postfix operator precedence issue


view this post on Zulip 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.

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

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.

view this post on Zulip 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.

view this post on Zulip 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