/Prelude-v18.0.0/List/generate.dhall

Copy path to clipboard

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)

Source

{-|
Build a list by calling the supplied function on all `Natural` numbers from `0`
up to but not including the supplied `Natural` number
-}
let generate
: Natural → ∀(a : Type) → (Natural → a) → List a
= λ(n : Natural) →
λ(a : Type) →
λ(f : Natural → a) →
List/build
a
( λ(list : Type) →
λ(cons : alistlist) →
List/fold
{ index : Natural, value : {} }
( List/indexed
{}
( List/build
{}
( λ(list : Type) →
λ(cons : {} → listlist) →
Natural/fold n list (cons {=})
)
)
)
list
(λ(x : { index : Natural, value : {} }) → cons (f x.index))
)

let example0 =
assert : generate 5 Bool Natural/even ≡ [ True, False, True, False, True ]

let example1 = assert : generate 0 Bool Natural/even ≡ ([] : List Bool)

in generate