- num_equal? = ???
- empty = \f n. n
- cons = \x xs. \f n. f x xs
- take_while = Y (\take_while. \p xs. xs (\y ys. (p y) (cons y (take_while p ys)) empty) empty)
- drop_while = Y (\drop_while. \p xs. xs (\y ys. (p y) (drop_while p ys) ys) empty)
+ ; `num_cmp x y lt eq gt` returns lt when x<y, eq when x==y, gt when x>y
+ let num_cmp = (\base build consume. \l r. r consume (l build base) fst)
+ ; where base is
+ (pair (\a b c. b) (K (\a b c. a)))
+ ; and build is
+ (\p. pair (\a b c. c) p)
+ ; and consume is
+ (\p. p fst p (p snd) (p snd)) in
+ let num_equal? = \x y. num_cmp x y false true false in
+ let neg = \b y n. b n y in
+ let empty = \f n. n in
+ let cons = \x xs. \f n. f x xs in
+ let empty? = \xs. xs (\y ys. false) true in
+ let tail = \xs. xs (\y ys. ys) empty in
+ let append = Y (\append. \xs zs. xs (\y ys. (cons y (append ys zs))) zs) in
+ let take_while = Y (\take_while. \p xs. xs (\y ys. (p y) (cons y (take_while p ys)) empty) empty) in
+ let drop_while = Y (\drop_while. \p xs. xs (\y ys. (p y) (drop_while p ys) xs) empty) in
+ ...