[Haskell-cafe] Proof format

2010-05-19 Thread R J
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 ={defi

Re: [Haskell-cafe] Proof format

2010-05-19 Thread Brent Yorgey
On Wed, May 19, 2010 at 01:12:16PM +, R J wrote: > > 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