[Haskell-cafe] (no subject)

[R J]

This is another proof-layout question, this time from Bird 1.4.7.
We're asked to define the functions curry2 and uncurry2 for currying and uncurrying functions with two arguments.  Simple enough:
curry2             :: ((a, b) -> c) -> (a -> (b -> c))curry2 f x y       =  f (x, y)
uncurry2           :: (a -> (b -> c)) -> ((a, b) -> c)uncurry2 f (x, y)  =  f x y
The following two assertions are obviously true theorems, but how are the formal proofs laid out?
1.  curry2 (uncurry2 f) x y = f x y
2.  uncurry2 (curry 2 f) (x, y) = f (x, y) 		 	   		  
_________________________________________________________________
The New Busy is not the too busy. Combine all your e-mail accounts with Hotmail.
http://www.windowslive.com/campaign/thenewbusy?tile=multiaccount&ocid=PID28326::T:WLMTAGL:ON:WL:en-US:WM_HMP:042010_4
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100519/cae08d30/attachment.html