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

main = case Nil of {
    Nil => 0 ;
    Cons a _ => a ;
};

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

--sum xs = case xs of {
--    Nil => 0 ;
--    Cons a xs => a + main xs ;
--};