[Haskell-cafe] Re: Induction (help!)

[Achim Schneider]

PR Stanley <prstanley at ntlworld.com> 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.