44 lines
916 B
Text
44 lines
916 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 : 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)
|
|
|
|
data a -> b where
|