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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
