Add size demo

This commit is contained in:
James Eversole
2025-01-23 18:57:59 -06:00
parent 2e246eb1c8
commit 8b043911ca
3 changed files with 23 additions and 1 deletions

19
demos/size.tri Normal file
View File

@ -0,0 +1,19 @@
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))