[Agda] Binding two identifiers using user-defined syntax

Andrés Sicard-Ramírez andres.sicard.ramirez at gmail.com
Thu Dec 1 14:51:40 CET 2011


On Thu, Dec 1, 2011 at 8:35 AM, Jean-Philippe Bernardy
<bernardy at chalmers.se> wrote:
> At the moment you need to have a constructor part between each "hole".
> E.g. this would work:
>
> syntax ∃₂ (λ x y → e) = ∃₂[ x , y ] e

It didn't work: Parse error y<ERROR> → e) = ∃₂[ x , y ] e ...

Best,

-- 
Andrés


More information about the Agda mailing list