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
	 James Eversole
						James Eversole