data List a where
    Cons : a -> List a -> List a
    Nil : List a

.++ xs ys = case xs of
    Nil => ys
    Cons z zs => Cons z (zs ++ ys)

length xs = case xs of
    Cons x xs => 1 + length xs

main = length (list1 ++ list2)

list1 = Cons 0 (Cons 1 (Cons 2 (Cons 3 Nil)))
list2 = Cons 4 (Cons 5 (Cons 6 (Cons 7 Nil)))