Does Gallina have an equivalent of Haskell's `$` or Ocaml's `@@`

132 Views Asked by At

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?

1

There are 1 best solutions below

0
On

I didn't test this, but it should work for a lot of contexts:

Notation "f @@ x" := (f x) (at level 10, x at level 100).

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.