Function-unfolding iterator

This module provides an infinite iterator that, given an initial value init and a function f, emits the iterates init, f init, f (f init), and so on.

@[unbox]

structure Std.Iterators.RepeatIterator (α : Type u) (f : α → α) : Type u

Internal state of the repeat combinator. Do not depend on its internals.

• next : α

  Internal implementation detail of the iterator library.

@[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]

def Std.Iterators.Iter.repeat {α : Type w} (f : α → α) (init : α) : Iter α

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 if 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 possible
• Productive instance: always

Equations

• Std.Iterators.Iter.repeat f init = { internalState := { next := init } }

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

Equations

• Std.Iterators.RepeatIterator.instIteratorLoop = Std.Iterators.IteratorLoop.defaultImplementation

instance Std.Iterators.RepeatIterator.instIteratorLoopPartial {α : Type w} {f : α → α} {n : Type w → Type w'} [Monad n] : IteratorLoopPartial (RepeatIterator α f) Id n

Equations

• Std.Iterators.RepeatIterator.instIteratorLoopPartial = Std.Iterators.IteratorLoopPartial.defaultImplementation

instance Std.Iterators.RepeatIterator.instIteratorCollect {α : Type w} {f : α → α} {n : Type w → Type w'} [Monad n] : IteratorCollect (RepeatIterator α f) Id n

Equations

• Std.Iterators.RepeatIterator.instIteratorCollect = Std.Iterators.IteratorCollect.defaultImplementation

instance Std.Iterators.RepeatIterator.instIteratorCollectPartial {α : Type w} {f : α → α} {n : Type w → Type w'} [Monad n] : IteratorCollectPartial (RepeatIterator α f) Id n

Equations

• Std.Iterators.RepeatIterator.instIteratorCollectPartial = Std.Iterators.IteratorCollectPartial.defaultImplementation