-- computes the sum of all numbers in a list
sum :: [Nat] -> Nat
sum [] = Z
sum [Z] = Z
sum [S Z] = S Z
sum [S(S Z)] = S(S Z)
sum [Z,Z] = Z
sum [Z,S Z] = S Z
sum [Z,S(S Z)] = S(S Z)
sum [S Z,Z] = S Z
sum [S Z,S Z] = S(S Z)
sum [S Z,S(S Z)] = S(S(S Z))
sum [S(S Z),Z] = S(S Z)
sum [S(S Z),S Z] = S(S(S Z))
sum [S(S Z),S(S Z)] = S(S(S(S Z)))
sum [S(S Z),S Z, S(S Z)] = S(S(S(S(S Z))))