Prefix priority which can supersede regular application

[yannl35133]

As far as I understand, regular application has infinite priority, so nothing can supersede it.

[fblanqui]

Thanks @yannl35133 to provide a use case.

[fblanqui]

@yannl35133 What is the status of this issue? You didn't answer my question yet.

[yannl35133]

I don't have a personal use-case, I don't need it currently.

As for a theoretical use-case, a prefix could always be replaced by a normal id, so it wouldn't be completely necessary; a use-case for an infix notation could be an operation lifted on functions, with a function called with parameters:

constant symbol Int: TYPE;
symbol +: Int → Int → Int;

symbol +! (f: Int → Int) (g: Int → Int) : Int → Int ≔ λ(x: Int), f x + g x;
notation +! infix left 1000; // more than application

type λ(x: Int), f +! g x;

I agree it does not feel natural here, most would just put parentheses around the addition, but it can be turned into something more convincing

[gabrielhdt]

Is this still relevant? Aren't we happy with the current behaviour being that function application has always the highest priority? Plus I think it would introduce some complexity regarding the user interface because users would have to remember what the application priority is, or we'd have to complexify the priority notation.