22 lines
295 B
Plaintext
22 lines
295 B
Plaintext
compose = f g x : f (g x)
|
|
|
|
succ = y (self :
|
|
triage
|
|
1
|
|
t
|
|
(triage
|
|
(t (t t))
|
|
(_ tail : t t (self tail))
|
|
t))
|
|
|
|
size = (x :
|
|
(y (self x :
|
|
compose succ
|
|
(triage
|
|
(x : x)
|
|
self
|
|
(x y : compose (self x) (self y))
|
|
x)) x 0))
|
|
|
|
size size
|