let x = 2;;
let y = 2;;
x y;;
let rec church n = fun f x -> if n = 0 then x else f (church (n - 1) f x);;
let zero = "";;
let succ = fun x -> "|" ^ x;;
church 5 succ zero;;
let add = fun m n f x -> m f (n f x);;
add (church 3) (church 6) succ zero;;
let exp = fun m n -> n m;;
exp (church 3) (church 3);;
exp (church 3) (church 3) succ zero;;
let y = fun f -> (fun x -> f (x x)) (fun x -> f (x x));;
let f x = x x;;



!def T = \x y. x
!def F = \x y. y
!def ite = \c t e. c t e
ite T x y
!trace
ite T x y
ite F x y
!def pair = \x y f. f x y
!def fst = \p. p T
fst (pair T F)
!def 0 = \f x. x
!def 1 = \f x. f x
!def 3 = \f x. f (f (f x))
!def add = \m n f x. m f (n f x)
add 3 3
!def exp = \m n. n m
exp 3 3
!def nil = \x. x
!def null = fst
null
null nil
!def Y = \f. (\x. f (x x)) (\x. f (x x))
!def len = Y (\f x. ite (null x) 0 (add 1 (f (tl x))))
length nil
!trace
length (cons 1 nil)
length (cons 1 (cons 1 nil))
len (cons 1 (cons 1 nil))