71 lines
		
	
	
		
			1.4 KiB
		
	
	
	
		
			Plaintext
		
	
	
	
	
	
			
		
		
	
	
			71 lines
		
	
	
		
			1.4 KiB
		
	
	
	
		
			Plaintext
		
	
	
	
	
	
| !import "base.tri" !Local
 | |
| 
 | |
| _ = t
 | |
| 
 | |
| matchList = a b : triage a _ b
 | |
| 
 | |
| emptyList? = matchList true (_ _ : false)
 | |
| head = matchList t (head _ : head)
 | |
| tail = matchList t (_ tail : tail)
 | |
| 
 | |
| append = y (self : matchList
 | |
|   (k : k)
 | |
|   (h r k : pair h (self r k)))
 | |
| 
 | |
| lExist? = y (self x : matchList
 | |
|   false
 | |
|   (h z : or? (equal? x h) (self x z)))
 | |
| 
 | |
| map_ = y (self :
 | |
|   matchList
 | |
|     (_ : t)
 | |
|     (head tail f : pair (f head) (self tail f)))
 | |
| map = f l : map_ l f
 | |
| 
 | |
| filter_ = y (self : matchList
 | |
|   (_ : t)
 | |
|   (head tail f : matchBool (t head) id (f head) (self tail f)))
 | |
| filter  = f l : filter_ l f
 | |
| 
 | |
| foldl_ = y (self f l x : matchList (acc : acc) (head tail acc : self f tail (f acc head)) l x)
 | |
| foldl  = f x l : foldl_ f l x
 | |
| 
 | |
| foldr_ = y (self x f l : matchList x (head tail : f (self x f tail) head) l)
 | |
| foldr  = f x l : foldr_ x f l
 | |
| 
 | |
| length = y (self : matchList
 | |
|   0
 | |
|   (_ tail : succ (self tail)))
 | |
| 
 | |
| reverse = y (self : matchList
 | |
|   t
 | |
|   (head tail : append (self tail) (pair head t)))
 | |
| 
 | |
| snoc = y (self x : matchList
 | |
|   (pair x t)
 | |
|   (h z : pair h (self x z)))
 | |
| 
 | |
| count = y (self x : matchList
 | |
|   0
 | |
|   (h z : matchBool
 | |
|     (succ (self x z))
 | |
|     (self x z)
 | |
|     (equal? x h)))
 | |
| 
 | |
| last = y (self : matchList
 | |
|   t
 | |
|   (hd tl : matchBool
 | |
|     hd
 | |
|     (self tl)
 | |
|     (emptyList? tl)))
 | |
| 
 | |
| all? = y (self pred : matchList
 | |
|   true
 | |
|   (h z : and? (pred h) (self pred z)))
 | |
| 
 | |
| any? = y (self pred : matchList
 | |
|   false
 | |
|   (h z : or? (pred h) (self pred z)))
 | |
| 
 | |
| intersect = xs ys : filter (x : lExist? x ys) xs
 |