1

Coq 中的 Gallina 语言是否有一个预定义的运算符来帮助避免像 Haskell's$或 OCaml's这样的括号@@？

如果没有，是否存在人们使用 Notation 定义的传统方法？

4

1 回答 1

1

我没有对此进行测试，但它应该适用于很多情况：

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

其要点是我们将参数表达式置于100最高级别，这意味着解析器开始将参数表达式 ( x) 解析为独立表达式。

10 级是函数应用程序的级别，所以你不想低于它，因为类似的东西hd 41 @@ [42; 43]不会解析。

于 2020-06-29T08:57:21.183 回答