## /Prelude-v23.0.0/Natural/fold.dhall

Copy path to clipboard

`fold` is the primitive function for consuming `Natural` numbers

If you treat the number `3` as `succ (succ (succ zero))` then a `fold` just replaces each `succ` and `zero` with something else

### Examples

`fold 3 Text (λ(x : Text) → "A" ++ x) "B" ≡ "AAAB"`

### Source

`{-|`fold` is the primitive function for consuming `Natural` numbersIf you treat the number `3` as `succ (succ (succ zero))` then a `fold` justreplaces each `succ` and `zero` with something else-}let fold    : Natural →      ∀(natural : Type) →      ∀(succ : natural → natural) →      ∀(zero : natural) →        natural    = Natural/foldlet example0 = assert : fold 3 Text (λ(x : Text) → "A" ++ x) "B" ≡ "AAAB"let example1 =      λ(zero : Text) →          assert        :   fold 3 Text (λ(x : Text) → "A" ++ x) zero          ≡ "A" ++ ("A" ++ ("A" ++ zero))let example2 =      λ(succ : Text → Text) →      λ(zero : Text) →        assert : fold 3 Text succ zero ≡ succ (succ (succ zero))in  fold`