uncurry

Stream: new members

[Manikhanta Teja]

i have been trying to write the uncurry function from exercise 2.10 and i'm having problems with it. I can understand what's wrong with it butI have no idea about what to do. Any help is appreciated.
Code :
def curry {alpha beta gamma : Type}
(f : (prod alpha beta) -> gamma) : alpha -> beta -> gamma
:= fun (x : alpha) (y : beta), f (x,y)
#check curry add1
def uncurry {alpha beta gamma : Type}
(f : alpha -> beta -> gamma) : (prod alpha beta) -> gamma
:= fun (x : alpha) (y : beta), f x y
Error:
type mismatch, term
λ (x : alpha) (y : beta), f x y
has type
alpha → beta → gamma
but is expected to have type
alpha × beta → gamma

[Mario Carneiro]

put code in triple backticks for formatting

[Mario Carneiro]

The function uncurry f takes a single argument of type prod alpha beta, so you should have fun p : prod alpha beta, ... to start. After that, you can use the projections p.fst and p.snd to extract the parts of type alpha and beta to pass to f

[Manikhanta Teja]

Thanks you so much. It worked.