churf/test_program
sebastianselander b08ae7aef1 rewrote unification for data type and variable.
could definitely be wrong. have to double check
2023-03-24 18:49:24 +01:00

46 lines
997 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;
-- };
deepList xs = case xs of {
Cons Nil _ => 1 ;
_ => 0 ;
};