!by_name
!def T = \x y . x
!def F = \x y . y
!def ite = \c x y . c x y
ite T x y
ite F x y
!def pair = \x y f
!def pair = \x y f . f x y
!def fst = \p. p T
!def snd = \p. p F
fst ( pair x y)
fst (pair T F)
snd (pair T F)
!def 0 = \f x . x
!def 1 = \f x . f x
!def 2 = \f x . f (f x)
!def add = \m n f x. m f (n f x)
add 2 2
!def 3 = \f x . f (f (f x))
add 3 3
!def pow = \m n. n m
pow 2 2
pow 3 3
!trace
pow 2 2
!def nil = \x . x
!def null = fst
null
!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))))
!def tl = \z. snd (snd z)
!def len = Y (\f x. ite (null x) 0 (add 1 (f (tl x))))
length nil
len nil
len