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