--- An example for verification with user-defined data types.

--- Natural numbers defined in Peano representation.
data Nat = Z | S Nat

--- Transforms a natural number into a standard integer.
fromNat :: Nat -> Int
fromNat Z     = 0
fromNat (S n) = 1 + fromNat n

--- Addition on natural numbers.
add :: Nat -> Nat -> Nat
add Z     n = n
add (S m) n = S(add m n)

--- The predecessor operation is partially defined.
pred :: Nat -> Nat
pred (S m) = m

pred'nonfail x = x/=Z

main = pred (S Z)