Is this how a rigorous Haskeller would lay out the proofs of the following
theorems? This is Bird 1.4.6.
(i)
Theorem: (*) x = (* x)
Proof:
(*) x = {definition of partial application} \y -> x * y =
{commutativity of "*"} \y -> y * x = {definition of "(* x)"} (* x)
(ii)
Theorem: (+) x = (x +)
Proof:
(+) x = {definition of partial application} \y -> x + y =
{definition of "(x +)"} (x +)
(iii)
Theorem: (-) x /= (- x)
Proof:
(-) x = {definition of partial application} \y -> x - y /=
{definition of prefix negation, which is not a section} (- x)
_________________________________________________________________
Hotmail is redefining busy with tools for the New Busy. Get more from your
inbox.
http://www.windowslive.com/campaign/thenewbusy?ocid=PID28326::T:WLMTAGL:ON:WL:en-US:WM_HMP:042010_2_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
