!module Size

!import "lib/base.tri" Lib

main = size size

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

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

size = (\x :
  (Lib.y (\self x :
    compose succ
      (Lib.triage
        (\x : x)
        self
        (\x y : compose (self x) (self y))
        x)) x 0))