43 lines
881 B
Text
43 lines
881 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);
|
|
|
|
deepPat xs = case xs of {
|
|
Cons (Nil) _ => True;
|
|
_ => False;
|
|
};
|
|
|
|
|