data N = Z | S (n:: N)

(+) (n,m:: N)
    :: N
    = case m of {
        (Z) -> n;
        (S m') -> S (n + m');}


list (A:: Set)
     :: Set
     = data nil | cons (a:: A)(l:: list A)


length (l :: list N)
       :: N
       = case l of {
           (nil) -> Z;
           (cons n l') -> S (length l);}


sumList (l :: list N)
       :: N
       = case l of {
           (nil) -> Z;
           (cons n l') -> n + sumList l';}