diff options
Diffstat (limited to 'std/List.bruijn')
| -rw-r--r-- | std/List.bruijn | 46 |
1 files changed, 23 insertions, 23 deletions
diff --git a/std/List.bruijn b/std/List.bruijn index 8e59ffd..1d43ecd 100644 --- a/std/List.bruijn +++ b/std/List.bruijn @@ -12,14 +12,14 @@ empty false # returns true if a list is empty empty? [0 [[[false]]] true] -<>?( empty? +<>?‣ empty? :test (<>?empty) (true) # prepends an element to a list cons P.pair -(:) cons +…:… cons :test ((+1) : ((+2) : empty)) (P.pair (+1) (P.pair (+2) empty)) :test (<>?((+2) : empty)) (false) @@ -27,14 +27,14 @@ cons P.pair # returns the head of a list or empty head P.fst -^( head +^‣ head :test (^((+1) : ((+2) : empty))) ((+1)) # returns the tail of a list or empty tail P.snd -~( tail +~‣ tail :test (~((+1) : ((+2) : empty))) ((+2) : empty) @@ -44,7 +44,7 @@ length z [[[rec]]] (+0) case-inc 2 ++1 ~0 case-end 1 -#( length +#‣ length :test (#((+1) : ((+2) : empty))) ((+2)) :test (#empty) ((+0)) @@ -55,7 +55,7 @@ index z [[[rec]]] case-index =?1 ^0 (2 --1 ~0) case-end empty -(!!) \index +…!!… \index :test (((+1) : ((+2) : ((+3) : empty))) !! (+0)) ((+1)) :test (((+1) : ((+2) : ((+3) : empty))) !! (+2)) ((+3)) @@ -68,8 +68,8 @@ foldl z [[[[rec]]]] case-fold 3 2 (2 1 ^0) ~0 case-end 1 -:test ((foldl (+) (+0) ((+1) : ((+2) : ((+3) : empty)))) =? (+6)) (true) -:test ((foldl (-) (+6) ((+1) : ((+2) : ((+3) : empty)))) =? (+0)) (true) +:test ((foldl add (+0) ((+1) : ((+2) : ((+3) : empty)))) =? (+6)) (true) +:test ((foldl sub (+6) ((+1) : ((+2) : ((+3) : empty)))) =? (+0)) (true) # foldl without starting value foldl1 [[foldl 1 ^0 ~0]] @@ -80,8 +80,8 @@ foldr [[[z [[rec]] 0]]] case-fold 4 ^0 (1 ~0) case-end 3 -:test ((foldr (+) (+0) ((+1) : ((+2) : ((+3) : empty)))) =? (+6)) (true) -:test ((foldr (-) (+2) ((+1) : ((+2) : ((+3) : empty)))) =? (+0)) (true) +:test ((foldr add (+0) ((+1) : ((+2) : ((+3) : empty)))) =? (+6)) (true) +:test ((foldr sub (+2) ((+1) : ((+2) : ((+3) : empty)))) =? (+0)) (true) # foldr without starting value foldr1 [[foldl 1 ^0 ~0]] @@ -89,7 +89,7 @@ foldr1 [[foldl 1 ^0 ~0]] # applies or to all list elements lor? foldr or? false -||( lor? +||‣ lor? :test (||(true : (true : empty))) (true) :test (||(true : (false : empty))) (true) @@ -98,7 +98,7 @@ lor? foldr or? false # applies and to all list elements land? foldr and? true -&&( land? +&&‣ land? :test (&&(true : (true : empty))) (true) :test (&&(true : (false : empty))) (false) @@ -112,7 +112,7 @@ product foldl mul (+1) :test (Π ((+1) : ((+2) : ((+3) : empty)))) ((+6)) # adds all values in list -sum foldl (+) (+0) +sum foldl add (+0) Σ sum @@ -131,7 +131,7 @@ lmin foldl1 min # reverses a list reverse foldl \cons empty -<~>( reverse +<~>‣ reverse :test (<~>((+1) : ((+2) : ((+3) : empty)))) ((+3) : ((+2) : ((+1) : empty))) @@ -145,14 +145,14 @@ append z [[[rec]]] case-merge ^1 : (2 ~1 0) case-end 0 -(++) append +…++… append :test (((+1) : ((+2) : ((+3) : empty))) ++ ((+4) : empty)) ((+1) : ((+2) : ((+3) : ((+4) : empty)))) # appends an element to a list snoc [[1 ++ (0 : empty)]] -(;) snoc +…;… snoc :test (empty ; (+1)) ((+1) : empty) :test (((+1) : empty) ; (+2)) ((+1) : ((+2) : empty)) @@ -163,7 +163,7 @@ map z [[[rec]]] case-map (1 ^0) : (2 1 ~0) case-end empty -(<$>) map +…<$>… map :test (inc <$> ((+1) : ((+2) : ((+3) : empty)))) ((+2) : ((+3) : ((+4) : empty))) @@ -173,7 +173,7 @@ filter z [[[rec]]] case-filter 1 ^0 (cons ^0) i (2 1 ~0) case-end empty -(<#>) \filter +…<#>… \filter :test (((+1) : ((+0) : ((+3) : empty))) <#> zero?) ((+0) : empty) @@ -183,7 +183,7 @@ last z [[rec]] case-last <>?(~0) ^0 (1 ~0) case-end empty -_( last +_‣ last :test (last ((+1) : ((+2) : ((+3) : empty)))) ((+3)) @@ -222,7 +222,7 @@ zip-with z [[[[rec]]]] case-zip <>?0 empty ((2 ^1 ^0) : (3 2 ~1 ~0)) case-end empty -:test (zip-with (+) ((+1) : ((+2) : empty)) ((+2) : ((+1) : empty))) ((+3) : ((+3) : empty)) +:test (zip-with add ((+1) : ((+2) : empty)) ((+2) : ((+1) : empty))) ((+3) : ((+3) : empty)) # returns first n elements of a list take z [[[rec]]] @@ -271,13 +271,13 @@ break [span (not! . 0)] :test (break (\(>?) (+3)) ((+1) : ((+2) : ((+4) : ((+1) : empty))))) (((+1) : ((+2) : empty)) : ((+4) : ((+1) : empty))) # returns true if any element in a list matches a predicate -any? [||( . (map 0)] +any? [||‣ . (map 0)] :test (any? (\gre? (+2)) ((+1) : ((+2) : ((+3) : empty)))) (true) :test (any? (\gre? (+2)) ((+1) : ((+2) : ((+2) : empty)))) (false) # returns true if all elements in a list match a predicate -all? [&&( . (map 0)] +all? [&&‣ . (map 0)] :test (all? (\gre? (+2)) ((+3) : ((+4) : ((+5) : empty)))) (true) :test (all? (\gre? (+2)) ((+4) : ((+3) : ((+2) : empty)))) (false) @@ -289,7 +289,7 @@ in? [[any? (\1 0)]] :test (in? (=?) (+0) ((+1) : ((+2) : ((+3) : empty)))) (false) # returns true if all elements of one list are equal to corresponding elements of other list -eq? &&( ... zip-with +eq? &&‣ ... zip-with :test (eq? (=?) ((+1) : ((+2) : empty)) ((+1) : ((+2) : empty))) (true) :test (eq? (=?) ((+1) : ((+2) : empty)) ((+2) : ((+2) : empty))) (false) |