16 lines
256 B
Text
16 lines
256 B
Text
data forall a. List (a) where {
|
|
Nil : List (a)
|
|
Cons : a -> List (a) -> List (a)
|
|
};
|
|
|
|
length : List (Int) -> Int;
|
|
length = \list. case list of {
|
|
Cons x xs => 1 + length xs;
|
|
-- Nil => 0;
|
|
-- Cons x (Cons y Nil) => 2;
|
|
};
|
|
|
|
|
|
|
|
|
|
|