false = t
_ = t
true = t t
k = t t
i = t (t k) t
s = t (t (k t)) t
m = s i i
b = s (k s) k
c = s (s (k s) (s (k k) s)) (k k)
iC = (\a b c : s a (k c) b)
iD = b (b iC) iC
iE = b (b iD) iC
yi = (\i : b m (c b (i m)))
y = yi iC
yC = yi iD
yD = yi iE
id = (\a : a)
triage = (\a b c : t (t a b) c)
pair = t
matchBool = (\ot of : triage of (\_ : ot) (\_ _ : ot))
matchList = (\oe oc : triage oe _ oc)
matchPair = (\op : triage _ _ op)
not = matchBool false true
and = matchBool id (\z : false)
if = (\cond then else : t (t else (t t then)) t cond)
test = triage "Leaf" (\z : "Stem") (\a b : "Fork")
emptyList = matchList true (\y z : false)
head = matchList t (\hd tl : hd)
tail = matchList t (\hd tl : tl)
lconcat = y (\self : matchList (\k : k) (\h r k : pair h (self r k)))
lAnd = triage (\x : false) (\_ x : x) (\_ _ x : x)
lOr = triage (\x : x) (\_ _ : true) (\_ _ x : true)
hmap = y (\self : matchList (\f : t) (\hd tl f : pair (f hd) (self tl f)))
map = (\f l : hmap l f)
equal = y (\self : triage (triage true (\z : false) (\y z : false)) (\ax : triage false (self ax) (\y z : false)) (\ax ay : triage false (\z : false) (\bx by : lAnd (self ax bx) (self ay by))))
hfilter = y (\self : matchList (\f : t) (\hd tl f : matchBool (t hd) i (f hd) (self tl f)))
filter = (\f l : hfilter l f)
hfoldl = y (\self f l x : matchList (\acc : acc) (\hd tl acc : self f tl (f acc hd)) l x)
foldl  = (\f x l : hfoldl f l x)
hfoldr = y (\self x f l : matchList x (\hd tl : f (self x f tl) hd) l)
foldr  = (\f x l : hfoldr x f l)