4 ; Cons : \/a. a -> List a -> List a
7 data Maybe : * -> * -> *
8 = { Left: \/a,b. a -> Maybe a b
9 ; Right: \/a,b. b -> Maybe a b
16 letrec { map: \/a,b. a -> b -> List a -> List b
21 ; Cons => \x:a, xx: List a.
22 Cons (f x) (map a b f xx)
27 letrec { reverse: \/a. List a -> List a
31 ; Cons x,xx => append (reverse xx) (Cons x Nil)
36 letrec { append: \/a. |~|_dummy:List a.|~|_:List a.List a
37 = /\a.\xs:List a, ys:List a.
40 ; Cons x:a,xx: List a => Cons x (append xx ys)