data N  = Z | S (n :: N)
-- False in Agda:
data False =

-- True in Agda:
data True = true


-- Less Than
(<) (n,m :: N)
    :: Set
     = case m of {
         (Z) -> False;
         (S m') -> case n of {
                     (Z) -> True;
                     (S n') -> n' < m';};}