## /Prelude-v19.0.0/List/fold.dhall

Copy path to clipboard

`fold` is the primitive function for consuming `List`s

If you treat the list `[ x, y, z ]` as `cons x (cons y (cons z nil))`, then a `fold` just replaces each `cons` and `nil` with something else

### Examples

`  fold Natural [ 2, 3, 5 ] Natural (λ(x : Natural) → λ(y : Natural) → x + y) 0≡ 10`
`  ( λ(nil : Natural) →      fold        Natural        [ 2, 3, 5 ]        Natural        (λ(x : Natural) → λ(y : Natural) → x + y)        nil  )≡ (λ(nil : Natural) → 2 + (3 + (5 + nil)))`
`  ( λ(list : Type) →    λ(cons : Natural → list → list) →    λ(nil : list) →      fold Natural [ 2, 3, 5 ] list cons nil  )≡ ( λ(list : Type) →    λ(cons : Natural → list → list) →    λ(nil : list) →      cons 2 (cons 3 (cons 5 nil))  )`

### Source

`{-|`fold` is the primitive function for consuming `List`sIf you treat the list `[ x, y, z ]` as `cons x (cons y (cons z nil))`, then a`fold` just replaces each `cons` and `nil` with something else-}let fold    : ∀(a : Type) →      List a →      ∀(list : Type) →      ∀(cons : a → list → list) →      ∀(nil : list) →        list    = List/foldlet example0 =        assert      :   fold            Natural            [ 2, 3, 5 ]            Natural            (λ(x : Natural) → λ(y : Natural) → x + y)            0        ≡ 10let example1 =        assert      :   ( λ(nil : Natural) →              fold                Natural                [ 2, 3, 5 ]                Natural                (λ(x : Natural) → λ(y : Natural) → x + y)                nil          )        ≡ (λ(nil : Natural) → 2 + (3 + (5 + nil)))let example2 =        assert      :   ( λ(list : Type) →            λ(cons : Natural → list → list) →            λ(nil : list) →              fold Natural [ 2, 3, 5 ] list cons nil          )        ≡ ( λ(list : Type) →            λ(cons : Natural → list → list) →            λ(nil : list) →              cons 2 (cons 3 (cons 5 nil))          )in  fold`