Documentation

Std.Data.Iterators.Producers.Repeat

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]
structure Std.Iterators.RepeatIterator (α : Type u) (f : αα) :

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 : αα} :
    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 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
    Instances For