diff options
Diffstat (limited to 'std/List.bruijn')
| -rw-r--r-- | std/List.bruijn | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/std/List.bruijn b/std/List.bruijn index 1f3d8f7..19fac6b 100644 --- a/std/List.bruijn +++ b/std/List.bruijn @@ -58,7 +58,7 @@ length z [[[rec]]] (+0) ⧗ (List a) → Number :test (∀((+1) : {}(+2))) ((+2)) :test (∀empty) ((+0)) -# applies each element of a list to a function +# applies each element of a list to a function (left-associative) apply z [[[rec]]] ⧗ (a* → b) → (List a) → b rec 0 [[[case-app]]] case-end case-app 5 (4 2) 1 @@ -68,13 +68,23 @@ apply z [[[rec]]] ⧗ (a* → b) → (List a) → b :test (…+… <! ((+1) : {}(+2))) ((+3)) -# applies each element of the tail to the head +# applies each element of the tail to the head (left-associative) eval [0 apply] ⧗ (Pair (a → b) (List a)) → b !‣ eval :test (!(…+… : ((+1) : {}(+2)))) ((+3)) +# applies each element of the tail to the head (right-associative) +eval-r z [[rec]] + rec 0 [[[case-app]]] case-end + case-app ∅?1 2 (2 (4 1)) + case-end 1 + +~!‣ eval-r + +:test (~!(inc : (inc : {}(+1)))) ((+3)) + # returns the element at index in list index z [[[rec]]] ⧗ (List a) → Number → a rec 0 [[[case-index]]] case-end |