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