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.

Equations

• Std.Iterators.ToIterator.iterM x = Std.Iterators.ToIterator.iterMInternal

@[inline]

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

Converts x into a pure iterator.

Equations

• Std.Iterators.ToIterator.iter x = (Std.Iterators.ToIterator.iterM x).toIter

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

Equations

• Std.Iterators.ToIterator.ofM State iterM = { State := State, iterMInternal := iterM }

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

Equations

• Std.Iterators.ToIterator.of State iter = { State := State, iterMInternal := iter.toIterM }

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 β

Equations

• Std.Iterators.instIteratorState = inferInstanceAs (Std.Iterators.Iterator State 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

Equations

• Std.Iterators.instIteratorCollectState = inferInstanceAs (Std.Iterators.IteratorCollect State 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

Equations

• Std.Iterators.instIteratorCollectPartialState = inferInstanceAs (Std.Iterators.IteratorCollectPartial State m n)

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

Equations

• Std.Iterators.instIteratorLoopState = inferInstanceAs (Std.Iterators.IteratorLoop State m n)

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

Equations

• Std.Iterators.instIteratorLoopPartialState = inferInstanceAs (Std.Iterators.IteratorLoopPartial State 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

Equations

• Std.Iterators.instIteratorSizeState = inferInstanceAs (Std.Iterators.IteratorSize State 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

Equations

• Std.Iterators.instIteratorSizePartialState = inferInstanceAs (Std.Iterators.IteratorSizePartial State m)