2025-01-27 16:04:04 -06:00
|
|
|
!module Size
|
|
|
|
|
|
|
|
!import "lib/base.tri" Lib
|
|
|
|
|
2025-01-26 15:33:12 -06:00
|
|
|
main = size size
|
|
|
|
|
2025-01-26 08:52:28 -06:00
|
|
|
compose = \f g x : f (g x)
|
2025-01-23 18:57:59 -06:00
|
|
|
|
2025-01-27 16:04:04 -06:00
|
|
|
succ = Lib.y (\self :
|
|
|
|
Lib.triage
|
2025-01-26 14:50:15 -06:00
|
|
|
1
|
|
|
|
t
|
2025-01-27 16:04:04 -06:00
|
|
|
(Lib.triage
|
2025-01-26 14:50:15 -06:00
|
|
|
(t (t t))
|
2025-01-27 16:04:04 -06:00
|
|
|
(\_ Lib.tail : t t (self Lib.tail))
|
2025-01-23 18:57:59 -06:00
|
|
|
t))
|
|
|
|
|
2025-01-26 14:50:15 -06:00
|
|
|
size = (\x :
|
2025-01-27 16:04:04 -06:00
|
|
|
(Lib.y (\self x :
|
2025-01-26 14:50:15 -06:00
|
|
|
compose succ
|
2025-01-27 16:04:04 -06:00
|
|
|
(Lib.triage
|
2025-01-26 14:50:15 -06:00
|
|
|
(\x : x)
|
|
|
|
self
|
|
|
|
(\x y : compose (self x) (self y))
|
2025-01-23 18:57:59 -06:00
|
|
|
x)) x 0))
|