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