Syntax binders with multi-argument lambdas

[GoogleCodeExporter]

The following example does not parse after commenting in one of the two lines
with the comment "Doesn't parse". It would be nice to be able to bind more than
one variable.

module SyntaxBug where

record Pair (A : Set)(B : A -> Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst
open Pair

split : {A : Set}{B : A -> Set}{P : (x : A) -> B x -> Set}(p : Pair A B)
        (f : (x : A) -> (y : B x) -> P x y) -> P (fst p) (snd p)
split (x , y) f = f x y

-- Doesn't parse
-- syntax split e (\ x y -> f) = e [ x ,, y ]=> f

-- Doesn't parse
-- syntax split e (\ x -> (\ y -> f)) = e [ x ,, y ]=> f

-- Parses
syntax split e (\ x -> f) = e [ x ]=> f

What version of Agda are you using? Latest darcs version.

Original issue reported on code.google.com by Fredriks...@gmail.com on 14 Mar 2011 at 4:16

[GoogleCodeExporter]

Original comment by nils.anders.danielsson on 15 Mar 2011 at 10:12

• Added labels: Priority-Medium, Type-Enhancement
• Removed labels: Type-Defect

[GoogleCodeExporter]

Has any progress been made on this front?

I've the latest version of Agda but it seems this issue is still unresolved :'(

Any advice would be most appreciated; thank you!

Original comment by alha...@gmail.com on 21 Jul 2015 at 9:51

[nad]

I seem to have sketched a way to do this.