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 ]

./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