tricu

An interpreted language for exploring Tree Calculus
Log | Files | Refs | README | LICENSE

size.tri (295B)


      1 compose = f g x : f (g x)
      2 
      3 succ = y (self :
      4   triage
      5     1
      6     t
      7     (triage
      8       (t (t t))
      9       (_ tail : t t (self tail))
     10       t))
     11 
     12 size = (x :
     13   (y (self x :
     14     compose succ
     15       (triage
     16         (x : x)
     17         self
     18         (x y : compose (self x) (self y))
     19         x)) x 0))
     20 
     21 size size