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

但是当我尝试定义绑定两个变量的自定义语法时，我得到一个错误

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 以获取相应的增强请求。