@@ c. (Combinator)
@@ def Y. (@ g.
  (@x.g (x x)) (@x.g (x x)))

@@ def I.(@x.x)
@@ def K.(@x y.x)
@@ def S.(@x y z.x z (y z))
@@ def B.(@x y z.x (y z))
@@ def C.(@x y z.x z y)
@@ def W.(@x y.x y y)
@@ def U.(@x.x x)
@@ def omega.U
@@ def OMEGA.(omega omega)

@@ c. (Logic)
@@ def #t.
  (@t f.t)
@@ def #f.
  (@t f.f)
@@ def 0?. (@ n.
  n (@x.#f) #t)
@@ def ?:. (@ p a b.
  p a b)
@@ def !. (@ p.
  @a b.p b a)
@@ def &. (@ p q.
  p q p)
@@ def |. (@ p q.
  p p q)
@@ def ^. (@ p q.
  p (! q) q)

@@ c. (Pairs)
@@ def pair. (@ x y.
  @f.f x y)
@@ def get0. (@ p.
  p #t)
@@ def get1. (@ p.
  p #f)
@@ def #nil.
  (@x.#t)
@@ def nil?. (@ p.
  p @x y.#f)

@@ c. (Arithmetic)
@@ def ++. (@ n.
  @f x.f (n f x))
@@ def +. (@ m n.
  m ++ n)
@@ def *. (@ m n.
  @f.m (n f))
@@ def **. (@ b e.
  e b)
@@ def --. (@ n.
  @f x.n (@g h.h (g f)) (@u.x) (@u.u))
@@ def -. (@ m n.
  n -- m)

@@ c. (Predicates)
@@ def <=. (@ m n.
  0? (- m n))
@@ def >=. (@ m n.
  <= n m)
@@ def >. (@ m n.
  ! (<= m n))
@@ def <. (@ m n.
  ! (>= m n))
@@ def =. (@ m n.
  & (<= m n) (>= m n))


@@ churchnums.


@@ c. (Math)
@@ def math:fact. (Y @Y_fact n.
  (0? n) 1
    (* (Y_fact (@@b.-- n)) n))

@@ def math:div. (@ n d.
  (0? d) #nil
    ((Y @Y_div d q r.
        (>= r d)
          (Y_div d (@@b.++ q) (@@b.- r d))
          (pair q r))
      d 0 n))



@@c. (Integers)

@@ def int:abs. (@ n.
  n @n0.pair #f)

@@ def int:neg. (@ n.
  n @n0.pair (! n0))

@@ def int:inc. (@ n.
  n @n0 n1.(0? n1)
    (pair #f 1)
    (pair n0
      ((n0 -- ++) n1)))

@@ def int:add. (@ m n.
  m @m0 m1.n @n0 n1.pair
    ((<= m1 n1) n0 m0)
    ((^ m0 n0)
      ((<= m1 n1)
        (- n1 m1)
        (- m1 n1))
      (+ m1 n1)))

@@ def int:dec. (@ n.
  n @n0 n1.(0? n1)
    (pair #t 1)
    (pair n0
      ((n0 ++ --) n1)))

@@ def int:sub. (@ m n.
  int:add m (int:neg n))

@@ def int:mul. (@ m n.
  m @m0 m1.n @n0 n1.pair
    (^ m0 n0)
    (* m1 n1))

@@ def int:zero?. (@ n.
  0? (get1 n))

@@ def int:neq?. (@ m n.
  m @m0 m1.n @n0 n1.
    (& (0? m1) (0? n1)) #f
      (| (^ m0 n0) (= m1 n1)))

@@ def int:leq?. (@ m n.
  m @m0 m1.n @n0 n1.
    (^ m0 n0)
      ((& (0? m1) (0? n1)) #t m0)
      ((m0 >= <=) m1 n1))



@@ c. (List)

@@ def list:append. (@ list list2.
  @e.list (list2 e))

@@ def list:appendx. (@ list x.
  list:append list (pair x))

@@ def list:del1. (@ list.
  @e.get1 (list e))

@@ def list:deln. (@ list n.
  @e.n get1 (list e))

@@ def list:pop1. (@ list.
  pair (list:del1 list)
    (get0 (list #e)))

@@ def list:popn. (Y @Y_pop list n dst.
  (0? n) (pair list dst)
    ((list:pop1 list) @list1 x.
        (Y_pop (@@b.list1) (@@b.-- n)
          (@@b.list:appendx dst x))))

@@ def list:getSlice. (@ list i n.
  get1 (list:popn
      (@@b.list:deln list i) n 1))

@@ def list:get. (@ list i.
  get0 (list:deln list i #e))

@@ def list:setSlice. (@ list i n list2.
  (list:popn list i 1) @sec0 sec1.
    list:append sec1 (list:append list2
        (list:deln sec0 n)))

@@ def list:set. (@ list i x.
  list:setSlice list i 1 (pair x))

@@ def list:delSlice. (@ list i n.
  list:setSlice list i n 1)

@@ def list:del. (@ list i.
  list:delSlice list i 1)

@@ def list:insert. (@ list i list2.
  list:setSlice list i 0 list2)

@@ def list:insertx. (@ list i x.
  list:insert list i (pair x))


@@ def list:repeat. (@ list n.
  n (list:append list) list)

@@ def list:length. (@ list.
  (Y @Y_len p n.
    (nil? p) n
      (Y_len (@@b.get1 p) (@@b.++ n)))
    (list #nil) 0)


@@ def list:applyAll. (@ func list.
  (Y @Y_aA func p.
    (nil? p) func
      (p @p0 p1.Y_aA (func p0) p1))
    func (list #nil))

@@ def list:_print. (@ list.
  list:applyAll [ (@@b.list) ])



@@ c. (Unsigned Decimal Integers)

@@ def uint10:_extp. (@ p.
  (nil? p) (pair 0 p) p)

@@ def uint10:_norm. (Y @Y_norm p s c.
  (& (nil? p) (0? c)) s
    ((uint10:_extp p) @p0 p1.
      (math:div (@@b.+ c p0) 10) @q r.
        Y_norm (@@b.p1)
          (@@b.list:appendx s r) q))

@@ def uint10:norm. (@ n.
  uint10:_norm (n #nil) 1 0)

@@ def uint10:inc. (@ n.
  (@e.(n e) @p0 p1.pair (++ p0) p1))

@@ def uint10:add. (@ m n.
  (Y @Y_add pm pn s.
    (& (nil? pm) (nil? pn)) s
      ((uint10:_extp pm) @pm0 pm1.
        (uint10:_extp pn) @pn0 pn1.
          Y_add (@@b.pm1) pn1
            (@@b.list:appendx s
              (@@b.+ pm0 pn0))))
    (m #nil) (n #nil) 1)