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 { -- 0 => True; -- _ => case xs of { -- Cons x xs => False; -- _ => False; -- }; -- }; -- _ => False; -- }; -- main = firstIsOne (Cons 1 Nil); test xs = case xs of { 1 => 0; lol => 1; };