35 lines
1.1 KiB
Text
35 lines
1.1 KiB
Text
{-|
|
|
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 : 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))
|
|
)
|
|
|
|
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
|