/Prelude-v23.0.0/List/iterate.dhall
Copy path to clipboardGenerate 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 ]
iterate 0 Natural (λ(x : Natural) → x * 2) 1 ≡ ([] : List Natural)
Source
{-|
Generate a list of the specified length given a seed value and transition
function
-}
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)
)
)
let example0 =
assert
: iterate 10 Natural (λ(x : Natural) → x * 2) 1
≡ [ 1, 2, 4, 8, 16, 32, 64, 128, 256, 512 ]
let example1 =
assert
: iterate 0 Natural (λ(x : Natural) → x * 2) 1 ≡ ([] : List Natural)
in iterate