data List (a) where {
    Nil : List (a)
    Cons : a -> List (a) -> List (a)
};

main = length (Cons 1 (Cons 2 Nil)) ;
id x = x;
const x y = x ;

map : (o -> g) -> List (o) -> List (g) ;
map f xs = case xs of {
    Nil => Nil ;
    Cons x xs => Cons (f x) (map f xs) ;
};

length : List (Int) -> Int ;
length xs = case xs of {
    Nil => 0 ;
    Cons _ xs => 1 + length xs ;
};

id_int : a -> b ;
id_int x = (x : a) ;