let true = \y n. y in
let false = \y n. n in
- let zero? = \n. n (\p. false) true in
- let pred = \n f z. n (\u v. v (u f)) (K z) I in
+ let pair = \a b. \v. v a b in
+ let fst = \a b. a in ; aka true
+ let snd = \a b. b in ; aka false
+ let zero = \s z. z in
let succ = \n s z. s (n s z) in
+ let zero? = \n. n (\p. false) true in
+ let pred = \n. n (\p. p (\a b. pair (succ a) a)) (pair zero zero) snd in
let add = \l r. r succ l in
let mult = \l r. r (add l) 0 in
let Y = \h. (\u. h (u u)) (\u. h (u u)) in
-->
; all functions from the previous question, plus
- let num_equal? = ??? in
+ ; `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