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

class Std.ToIterator (γ : Type u) (m : Type w → Type w') (α β : outParam (Type w)) : Type (max u w)

This typeclass provides an iterator for elements of type γ.

• iterMInternal (x : γ) : IterM m β

@[inline]

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

Converts x into a monadic iterator.

Equations

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

@[inline]

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

Converts x into a pure iterator.

Equations

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

@[instance_reducible, inline]

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

Creates a monadic ToIterator instance.

Equations

• Std.ToIterator.ofM α iterM = { iterMInternal := fun (x : γ) => iterM x }

@[instance_reducible, inline]

def Std.ToIterator.of {γ : Type u_1} {β : Type w} (α : Type w) (iter : γ → Iter β) : ToIterator γ Id α β

Creates a pure ToIterator instance.

Equations

• Std.ToIterator.of α iter = { iterMInternal := fun (x : γ) => (iter x).toIterM }

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

Replaces ToIterator.iterM with its definition.

theorem Std.ToIterator.iter_eq {γ : Type u} {x : γ} {α β : Type v} {it : γ → IterM Id β} : iter x = (it x).toIter

Replaces ToIterator.iter with its definition.