## /Prelude-v23.0.0/List/iterate.dhall

Copy path to clipboard

Generate a list of the specified length given a seed value and transition function

### Examples

`  iterate 10 Natural (λ(x : Natural) → x * 2) 1≡ [ 1, 2, 4, 8, 16, 32, 64, 128, 256, 512 ]`
`iterate 0 Natural (λ(x : Natural) → x * 2) 1 ≡ ([] : List Natural)`

### Source

`{-|Generate a list of the specified length given a seed value and transitionfunction-}let iterate    : Natural → ∀(a : Type) → (a → a) → a → List a    = λ(n : Natural) →      λ(a : Type) →      λ(f : a → a) →      λ(x : a) →        List/build          a          ( λ(list : Type) →            λ(cons : a → list → list) →              List/fold                { index : Natural, value : {} }                ( List/indexed                    {}                    ( List/build                        {}                        ( λ(list : Type) →                          λ(cons : {} → list → list) →                            Natural/fold n list (cons {=})                        )                    )                )                list                ( λ(y : { index : Natural, value : {} }) →                    cons (Natural/fold y.index a f x)                )          )let example0 =        assert      :   iterate 10 Natural (λ(x : Natural) → x * 2) 1        ≡ [ 1, 2, 4, 8, 16, 32, 64, 128, 256, 512 ]let example1 =        assert      : iterate 0 Natural (λ(x : Natural) → x * 2) 1 ≡ ([] : List Natural)in  iterate`