Does the Gallina language in Coq have a predefined operator that helps avoid parentheses like Haskell's $
or OCaml's @@
?
If not, is there a conventional one that people define using Notation?
Does the Gallina language in Coq have a predefined operator that helps avoid parentheses like Haskell's $
or OCaml's @@
?
If not, is there a conventional one that people define using Notation?
Copyright © 2021 Jogjafile Inc.
I didn't test this, but it should work for a lot of contexts:
The gist of this is that we put the argument expression at the level
100
which is the highest level, meaning the parser kind of starts parsing the argument expression (x
) as a standalone expression.The level 10 is the level of function application, so you don't want to go below that because something like
hd 41 @@ [42; 43]
wouldn't parse.