I don't understand your goal. Isn't Peano arithmetic summarized in Haskell as:
data Peano = Zero | Succ Peano deriving Eq This corresponds to a first-order logic over a signature that has equality, a constant symbol 0, and a one-place successor function symbol S. Function symbols such as < and + can be introduced as defined function symbols that do not add substantive information to the theory. The only axioms you want are the ones for equality. John _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
