tricu/lib/base.tri

false = t
_     = t
true  = t t
id    = \a : a
const = \a b : a
pair  = t
if    = \cond then else : t (t else (t t then)) t cond

y = ((\mut wait fun : wait mut (\x : fun (wait mut x)))
     (\x : x x)
     (\a0 a1 a2 : t (t a0) (t t a2) a1))

compose = \f g x : f (g x)

triage = \leaf stem fork : t (t leaf stem) fork
test   = triage "Leaf" (\_ : "Stem") (\_ _ : "Fork")

matchBool = (\ot of : triage
  of
  (\_ : ot)
  (\_ _ : ot)
)

lAnd = (triage
  (\_     : false)
  (\_ x   : x)
  (\_ _ x : x))

lOr = (triage
  (\x     : x)
  (\_ _   : true)
  (\_ _ _ : true))

matchPair = \a : triage _ _ a

not? = matchBool false true
and? = matchBool id (\_ : false)

or? = (\x z : 
  matchBool 
    (matchBool true true z)
    (matchBool true false z)
    x)

xor? = (\x z : 
  matchBool 
    (matchBool false true z)
    (matchBool true false z)
    x)

equal? = y (\self : triage
  (triage
    true
    (\_   : false)
    (\_ _ : false))
  (\ax :
    triage
      false
      (self ax)
      (\_ _ : false))
  (\ax ay :
    triage
      false
      (\_ : false)
      (\bx by : lAnd (self ax bx) (self ay by))))

succ = y (\self :
  triage
    1
    t
    (triage
      (t (t t))
      (\_ tail : t t (self tail))
      t))