You can't have negative numbers with that definition. Here are numbers and the way you would write them with that definition:
0 == Z
1 == Suc Z
2 == Suc (Suc Z)
3 == Suc (Suc (Suc Z))
You can define some arithmetic operators for it:
data Nat = Z | Suc Nat deriving (Show, Eq)
instance Num Nat where
(Suc x) + y = Suc (x + y)
Z + y = y
(Suc x) - (Suc y) = x - y
x - Z = x
Z - (Suc _) = undefined
Z * y = Z
(Suc x) * y = (x * y) + y
negate = undefined
abs x = x
signum (Suc _) = Suc Z
signum Z = Z
fromInteger 0 = Z
fromInteger x
| x < 0 = undefined
| otherwise = Suc (fromInteger (x - 1))
The definition `fromInteger` is used by GHC to implicitly convert decimal numbers in the code to our Nat. We can use it like this:
ghci> 0 == Z
True
ghci> 1 == Suc Z
True
ghci> 2 == Suc (Suc Z)
True
ghci> 3 :: Nat
Suc (Suc (Suc Z))
ghci> 3 + 2 :: Nat
Suc (Suc (Suc (Suc (Suc Z))))
ghci> 3 - 2 :: Nat
Suc Z
ghci> 3 * 2 :: Nat
Suc (Suc (Suc (Suc (Suc (Suc Z)))))
ghci> 3 - 4 :: Nat
*** Exception: Prelude.undefined
CallStack (from HasCallStack):
error, called at libraries/base/GHC/Err.hs:78:14 in base:GHC.Err
undefined, called at <interactive>:70:15 in interactive:Ghci8
It looks like it is trying to do something like (from your link) Coq's
But obviously defining natural numbers in terms of Z/the integers doesn't work because I could then call -1 a natural number.