41 lines
919 B
Text
41 lines
919 B
Text
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;
|
|
};
|