Add size demo
This commit is contained in:
19
demos/size.tri
Normal file
19
demos/size.tri
Normal 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))
|
Reference in New Issue
Block a user