iterate

{-
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] : List Natural

./iterate +0 Natural (λ(x : Natural) → x * +2) +1
= [] : List Natural
```
-}
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)
            )
        )

in  iterate