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

data Bool () where {
    True : Bool ()
    False : Bool ()
   };

-- hello_world = Cons 'h' (Cons 'e' (Cons 'l' (Cons 'l' (Cons 'o' (Cons ' ' (Cons 'w' (Cons 'o' (Cons 'r' (Cons 'l' (Cons 'd' Nil)))))))))) ;

-- length : List (a) -> Int ;
-- length xs = case xs of {
--     Nil => 0 ;
--     Cons x xs => length xs
-- };

-- head : List (a) -> a ;
-- head xs = case xs of {
--     Cons x xs => x
-- };

firstIsOne : List (Int) -> Bool () ;
firstIsOne xs = case xs of {
    Cons x xs => case x of {
            1 => True ;
            _ => case xs of {
                    Cons x xs => False ;
                    _ => False
                }
            };
    _ => False
    };

-- firstIsOne :: [Int] -> Bool 
-- firstIsOne xs = case xs of
--     (1 : xs) -> True
--     _ -> False

main = firstIsOne (Cons 'a' Nil)