generate

{-
Build a list by calling the supplied function on all `Natural` numbers from `+0`
up to but not including the supplied `Natural` number

Examples:

```
./generate +5 Bool Natural/even = [True, False, True, False, True] : List Bool

./generate +0 Bool Natural/even = [] : List Bool
```
-}
let generate : Natural → ∀(a : Type) → (Natural → a) → List a
    =   λ(n : Natural)
    →   λ(a : Type)
    →   λ(f : Natural → 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
            (λ(x : { index : Natural, value : {} }) → cons (f x.index))
        )

in  generate