import nat
import pair
def head : List -> Nat = fun xs =>
match xs
with nil => ?{head of empty list}
with cons x xs' => x
def tail : List -> List = fun xs =>
match xs
with nil => ?{tail of empty list}
with cons x xs' => xs'
def length : List -> Nat = fun xs =>
match xs
with nil => zero
with cons x xs' => succ (length xs')
def map : (Nat -> Nat) -> List -> List = fun f xs =>
match xs
with nil => nil
with cons x xs' => cons (f x) (map f xs')
def filter : (Nat -> Bool) -> List -> List = fun p xs =>
match xs
with nil => nil
with cons x xs' => (
match p x
with true => cons x (filter p xs')
with false => filter p xs'
)
def fold : Nat -> (Nat -> Nat -> Nat) -> List -> Nat = fun z s xs =>
match xs
with nil => z
with cons x xs' => s z (fold z s xs')
def up_to_iter : Nat -> Nat -> List = fun n k =>
match k
with zero => nil
with succ k' =>
let r = sub n k
in cons r (up_to_iter n k')
def up_to : Nat -> List = fun n => up_to_iter n n
def take : Nat -> List -> List = fun n xs =>
match n
with zero => nil
with succ n' => (
match xs
with nil => nil
with cons x xs' => cons x (take n' xs)
)
def one_two_three : List =
cons one (cons two (cons three nil))
def main : Top = println (show (length (one_two_three)))