module tuple where


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

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




infix 20 _::_

data Tuple (A : Set):  ℕ -> Set where
  []    : Tuple A Z
  _::_  : {n : ℕ} -> A -> Tuple A n -> Tuple A (S n)


sumℕTuple : {n : ℕ} -> Tuple ℕ n -> Tuple ℕ n -> Tuple ℕ n
sumℕTuple []       []          = []
sumℕTuple (m :: l) (m' :: l')  = m + m' :: sumℕTuple l l'