[Agda] Binding two identifiers using user-defined syntax

[Andrés Sicard-Ramírez]

Hi,

Using the support for declare user-defined syntax, I can define for example

  postulate D

  data ∃ (P : D → Set) : Set where
    _,_ : (x : D) → P x → ∃ P

  syntax ∃ (λ x → e) = ∃[ x ] e

but if I want to define something similar for the data type

  data ∃₂ (P : D → D → Set) : Set where
    _,_,_ : (x y : D) → P x y → ∃₂ P

the syntax declaration

    syntax ∃₂ (λ x y → e) = ∃₂[ x y ] e

yields a parse error. Is it possible to bind two identifiers using a
syntax declaration?

Thanks,

-- 
Andrés