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