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
      @[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
          instance Std.Iterators.RepeatIterator.instIteratorLoop {α : Type w} {f : αα} {n : Type w → Type w'} [Monad n] :
          Equations
            instance Std.Iterators.RepeatIterator.instIteratorLoopPartial {α : Type w} {f : αα} {n : Type w → Type w'} [Monad n] :
            Equations
              instance Std.Iterators.RepeatIterator.instIteratorCollect {α : Type w} {f : αα} {n : Type w → Type w'} [Monad n] :
              Equations
                Equations