\section{Inductive Definition of Natural Numbers}

\begin{code}
module NatNum where
import Data.Typeable

data Nat = Zero | Succ
  deriving Typeable
\end{code}