Documentation

Std.Data.Iterators.Producers.Repeat

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.

@[inline]
instance Std.Iterators.instIteratorRepeatIteratorId {α : Type w} {f : αα} :
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