Hi,
Below are two attempts to define Peano arithmetic in Haskell.
The first attempt, Peano1, consists of just a signature in the class
with the axioms in the instance. In the second attempt, Peano2, I am
trying to move the axioms into the class. The reason is, I want to put
as much specification
The problem is that you are using 'suc' as if it is a constructor: ((suc m)
`eq` (suc n) = m `eq` n)
You'll have to change it to something else, and it will probably require
adding an unpacking function to your class and it will probably be messy.
I'd suggest you make use of the Eq typeclass and
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
