Function-unfolding iterator #
This module provides an infinite iterator that given an initial value init
function f
emits
the iterates init
, f init
, f (f init)
, ... .
@[unbox]
Internal state of the repeat
combinator. Do not depend on its internals.
- next : α
Internal implementation detail of the iterator library.
Instances For
@[inline]
instance
Std.Iterators.instIteratorRepeatIteratorId
{α : Type w}
{f : α → α}
:
Iterator (RepeatIterator α f) Id α
Equations
- One or more equations did not get rendered due to their size.
@[inline]
Creates an infinite iterator from an initial value init
and a function f : α → α
.
First it yields init
, and in each successive step, the iterator applies f
to the previous value.
So the iterator just emitted a
, in the next step it will yield f a
. In other words, the
n
-th value is Nat.repeat f n init
.
For example, if f := (· + 1)
and init := 0
, then the iterator emits all natural numbers in
order.
Termination properties:
Finite
instance: not available and never possibleProductive
instance: always
Instances For
instance
Std.Iterators.RepeatIterator.instProductive
{α : Type w}
{f : α → α}
:
Productive (RepeatIterator α f) Id
instance
Std.Iterators.RepeatIterator.instIteratorLoop
{α : Type w}
{f : α → α}
{n : Type w → Type w'}
[Monad n]
:
IteratorLoop (RepeatIterator α f) Id n
instance
Std.Iterators.RepeatIterator.instIteratorLoopPartial
{α : Type w}
{f : α → α}
{n : Type w → Type w'}
[Monad n]
:
IteratorLoopPartial (RepeatIterator α f) Id n
instance
Std.Iterators.RepeatIterator.instIteratorCollect
{α : Type w}
{f : α → α}
{n : Type w → Type w'}
[Monad n]
:
IteratorCollect (RepeatIterator α f) Id n
instance
Std.Iterators.RepeatIterator.instIteratorCollectPartial
{α : Type w}
{f : α → α}
{n : Type w → Type w'}
[Monad n]
:
IteratorCollectPartial (RepeatIterator α f) Id n