PR Stanley <[EMAIL PROTECTED]> wrote:

> Hi
> One of you chaps mentioned the Nat data type
> data Nat = Zero | Succ Nat
> 
> Let's have
> add :: Nat -> Nat -> Nat
> add Zero n = n
> add (Succ m)n = Succ (add m n)
> 
> Prove
> add m Zero = m
> 
> I'm on the verge of giving up on this. :-(
>

The important point is to learn to regard an infinite number of
terms as one term, and how to mess with it without allowing individual
terms to escape or dangle around.

-- 
(c) this sig last receiving data processing entity. Inspect headers for
past copyright information. All rights reserved. Unauthorised copying,
hiring, renting, public performance and/or broadcasting of this
signature prohibited. 

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to