module list where
  
infixr 30 _::_
data List (A : Set) : Set where
   []    : List A
   _::_  : A -> List A -> List A


postulate A : Set
postulate C : List A -> Set


f : (l : List A)  -> C l
f []       = {! !}
f (a :: l) = {! !}


data ℕ : Set where
  Z : ℕ
  S : ℕ -> ℕ

{-# BUILTIN NATURAL  ℕ  #-}

infixr 40 _+_

_+_ : ℕ -> ℕ -> ℕ
n + Z   = n
n + S m = S (n + m)

 


length : List ℕ -> ℕ 
length []       = Z
length (_ :: l) = S (length l)


sumlist : List ℕ -> ℕ 
sumlist [] = Z
sumlist (n :: l)  = n + sumlist l

infixr 20 _++_

_++_ : {A : Set} -> List A -> List A -> List A
[]       ++ l' = l'
a :: l   ++ l' = a :: (l ++ l')