syntax - Agda 中自定义语法声明的规则是什么？

Question

Agda docs在 syntax 声明上真的没什么好说的，粗略地浏览一下源代码并不能说明问题，所以我一直在尝试使用标准库中的示例自己将它拼凑起来，比如Σ[_]_ 和 ∃[_]_。我可以很容易地重现像他们这样的(诚然相当做作的)例子

twice : {A : Set} → (A → A) → A → A
twice f x = f (f x)

syntax twice (λ x → body) = twice[ x ] body

但是当我尝试定义绑定(bind)两个变量的自定义语法时，出现错误

swap : {A B C : Set} → (A → B → C) → B → A → C
swap f y x = f x y

syntax swap (λ x y → body) = swap[ x , y ] body

具体而言，

Parse error
y<ERROR>
 → body) = swap[ x , y ] body
...

所以我假设有一些关于 syntax 声明左侧允许的内容的规则。这些规则是什么，其中哪些禁止我上面的双变量 lambda 形式？

Answer 1

目前 Agda 不允许使用多参数 lambda 抽象的语法声明。这是一个已知限制，请参阅 issue tracker用于相应的增强请求。