Allow multiline expressions
This commit is contained in:
78
lib/base.tri
78
lib/base.tri
@ -17,25 +17,77 @@ 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)
|
||||
|
||||
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)))
|
||||
|
||||
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))))
|
||||
|
||||
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)
|
||||
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)
|
||||
|
Reference in New Issue
Block a user