This module provides the typeclass ToIterator, which is implemented by types that can be converted into iterators.

class Std.Iterators.ToIterator {γ : Type u} (x : γ) (m : Type w → Type w') (β : outParam (Type w)) : Type (w + 1)

This typeclass provides an iterator for the given element x : γ. Usually, instances are provided for all elements of a type γ.

• State : Type w
• iterMInternal : IterM m β

@[inline]

def Std.Iterators.ToIterator.iterM {γ : Type u_1} {m : Type u_2 → Type u_3} {β : Type u_2} (x : γ) [ToIterator x m β] : IterM m β

Converts x into a monadic iterator.

@[inline]

def Std.Iterators.ToIterator.iter {γ : Type u_1} {β : Type u_2} (x : γ) [ToIterator x Id β] : Iter β

Converts x into a pure iterator.

@[inline]

def Std.Iterators.ToIterator.ofM {γ : Type u_1} {m : Type w → Type u_2} {β : Type w} {x : γ} (State : Type w) (iterM : IterM m β) : ToIterator x m β

Creates a monadic ToIterator instance.

@[inline]

def Std.Iterators.ToIterator.of {γ : Type u_1} {β : Type w} {x : γ} (State : Type w) (iter : Iter β) : ToIterator x Id β

Creates a pure ToIterator instance.

theorem Std.Iterators.ToIterator.iterM_eq {γ : Type u} {x : γ} {State β : Type v} {it : IterM Id β} : iterM x = it

theorem Std.Iterators.ToIterator.iter_eq {γ : Type u} {x : γ} {State β : Type v} {it : IterM Id β} : iter x = it.toIter

Instance forwarding

If the type defined as ToIterator.State implements an iterator typeclass, then this typeclass should also be available when the type is syntactically visible as ToIteratorState. The following instances are responsible for this forwarding.

instance Std.Iterators.instIteratorState {γ : Type u_1} {m : Type w → Type u_2} {β : Type w} {x : γ} {State : Type w} {iter : IterM m β} [Iterator State m β] : Iterator (ToIterator.State x m) m β

instance Std.Iterators.instFiniteState {γ : Type u_1} {m : Type w → Type u_2} {β : Type w} {x : γ} {State : Type w} {iter : IterM m β} [Iterator State m β] [Finite State m] : Finite (ToIterator.State x m) m

instance Std.Iterators.instIteratorCollectState {γ : Type u_1} {m : Type w → Type u_2} {β : Type w} {n : Type w → Type u_3} {x : γ} {State : Type w} {iter : IterM m β} [Iterator State m β] [IteratorCollect State m n] : IteratorCollect (ToIterator.State x m) m n

instance Std.Iterators.instIteratorCollectPartialState {γ : Type u_1} {m : Type w → Type u_2} {β : Type w} {n : Type w → Type u_3} {x : γ} {State : Type w} {iter : IterM m β} [Iterator State m β] [IteratorCollectPartial State m n] : IteratorCollectPartial (ToIterator.State x m) m n

instance Std.Iterators.instIteratorLoopState {γ : Type u_1} {m : Type w → Type u_2} {β : Type w} {n : Type w → Type u_3} {x : γ} {State : Type w} {iter : IterM m β} [Iterator State m β] [IteratorLoop State m n] : IteratorLoop (ToIterator.State x m) m n

instance Std.Iterators.instIteratorLoopPartialState {γ : Type u_1} {m : Type w → Type u_2} {β : Type w} {n : Type w → Type u_3} {x : γ} {State : Type w} {iter : IterM m β} [Iterator State m β] [IteratorLoopPartial State m n] : IteratorLoopPartial (ToIterator.State x m) m n

instance Std.Iterators.instIteratorSizeState {γ : Type u_1} {m : Type w → Type u_2} {β : Type w} {x : γ} {State : Type w} {iter : IterM m β} [Iterator State m β] [IteratorSize State m] : IteratorSize (ToIterator.State x m) m

instance Std.Iterators.instIteratorSizePartialState {γ : Type u_1} {m : Type w → Type u_2} {β : Type w} {x : γ} {State : Type w} {iter : IterM m β} [Iterator State m β] [IteratorSizePartial State m] : IteratorSizePartial (ToIterator.State x m) m