structure Std.Iterators.BundledIterM (m : Type w → Type w') (β : Type w) : Type (max (w + 1) w')

A type with an iterator typeclass and an inhabitant bundled together. This represents an arbitrarily typed iterator. It only exists for the construction of the equivalence relation on iterators.

This type is not meant to be used in executable code. Unbundled Iter or IterM iterators of a specific type have better library support and are more efficient.

• α : Type w
• inst : Iterator self.α m β
• iterator : IterM m β

def Std.Iterators.BundledIterM.ofIterM {m : Type u_1 → Type u_2} {β α : Type u_1} [Iterator α m β] (it : IterM m β) : BundledIterM m β

Equations

• Std.Iterators.BundledIterM.ofIterM it = { α := α, inst := inferInstance, iterator := it }

@[simp]

theorem Std.Iterators.BundledIterM.iterator_ofIterM {m : Type u_1 → Type u_2} {β α : Type u_1} [Iterator α m β] (it : IterM m β) : (ofIterM it).iterator = it

instance Std.Iterators.instIteratorα {m : Type u_1 → Type u_2} {β : Type u_1} (bit : BundledIterM m β) : Iterator bit.α m β

Equations

• Std.Iterators.instIteratorα bit = bit.inst

noncomputable def Std.Iterators.IterM.stepAsHetT {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Iterator α m β] [Monad m] (it : IterM m β) : HetT m (IterStep (IterM m β) β)

A noncomputable variant of IterM.step using the HetT monad. It is used in the definition of the equivalence relations on iterators, namely IterM.Equiv and Iter.Equiv.

Equations

• it.stepAsHetT = { Property := it.IsPlausibleStep, small := ⋯, operation := (fun (step : Subtype it.IsPlausibleStep) => Std.Internal.USquash.deflate step) <$> it.step }

noncomputable def Std.Iterators.BundledIterM.step {β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] (it : BundledIterM m β) : HetT m (IterStep (BundledIterM m β) β)

Equations

• it.step = Std.Iterators.HetT.map (Std.Iterators.IterStep.mapIterator Std.Iterators.BundledIterM.ofIterM) it.iterator.stepAsHetT

@[irreducible]

def Std.Iterators.BundledIterM.Equiv (m : Type w → Type w') (β : Type w) [Monad m] [LawfulMonad m] (ita itb : BundledIterM m β) : Prop

Equivalence relation on bundled iterators.

Two bundled iterators are equivalent if they have the same Iterator.IsPlausibleStep relation and their step functions are the same up to equivalence of the successor iterators. This coinductive definition captures the idea that the only relevant feature of an iterator is its step function. Other information retrievable from the iterator -- for example, whether it is a list iterator or an array iterator -- is totally irrelevant for the equivalence judgement.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Std.Iterators.Equivalence.prun_liftInner_step {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} {n : Type u_1 → Type u_3} {γ : Type u_1} [Iterator α m β] [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n] {it : IterM m β} {f : (step : IterStep (IterM m β) β) → (HetT.liftInner n it.stepAsHetT).Property step → n γ} : (HetT.liftInner n it.stepAsHetT).prun f = do let step ← liftM it.step f step.val ⋯

@[simp]

theorem Std.Iterators.Equivalence.property_step {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Iterator α m β] [Monad m] [LawfulMonad m] {it : IterM m β} : it.stepAsHetT.Property = it.IsPlausibleStep

@[simp]

theorem Std.Iterators.Equivalence.prun_step {α : Type u_1} {m : Type u_1 → Type u_2} {β γ : Type u_1} [Iterator α m β] [Monad m] [LawfulMonad m] {it : IterM m β} {f : (step : IterStep (IterM m β) β) → it.stepAsHetT.Property step → m γ} : it.stepAsHetT.prun f = do let step ← it.step f step.val ⋯

noncomputable def Std.Iterators.BundledIterM.stepOnQuotient {β : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] : Quot (Equiv m β) → HetT m (IterStep (Quot (Equiv m β)) β)

Like BundledIterM.step, but takes and returns iterators modulo BundledIterM.Equiv.

Equations

• One or more equations did not get rendered due to their size.

theorem Std.Iterators.BundledIterM.stepOnQuotient_mk {m : Type w → Type w'} [Monad m] [LawfulMonad m] {β : Type w} [Monad m] [LawfulMonad m] {bit : BundledIterM m β} : stepOnQuotient (Quot.mk (Equiv m β) bit) = IterStep.mapIterator (Quot.mk (Equiv m β)) <$> bit.step

theorem Std.Iterators.BundledIterM.Equiv.exact {m : Type w → Type w'} {β : Type w} [Monad m] [LawfulMonad m] (ita itb : BundledIterM m β) : Quot.mk (Equiv m β) ita = Quot.mk (Equiv m β) itb → Equiv m β ita itb

theorem Std.Iterators.BundledIterM.Equiv.quotMk_eq_iff {m : Type w → Type w'} {β : Type w} [Monad m] [LawfulMonad m] (ita itb : BundledIterM m β) : Quot.mk (Equiv m β) ita = Quot.mk (Equiv m β) itb ↔ Equiv m β ita itb

theorem Std.Iterators.BundledIterM.Equiv.refl {m : Type w → Type w'} {β : Type w} [Monad m] [LawfulMonad m] (it : BundledIterM m β) : Equiv m β it it

theorem Std.Iterators.BundledIterM.Equiv.symm {m : Type w → Type w'} {β : Type w} [Monad m] [LawfulMonad m] {ita itb : BundledIterM m β} (h : Equiv m β ita itb) : Equiv m β itb ita

theorem Std.Iterators.BundledIterM.Equiv.trans {m : Type w → Type w'} {β : Type w} [Monad m] [LawfulMonad m] {ita itb itc : BundledIterM m β} (hab : Equiv m β ita itb) (hbc : Equiv m β itb itc) : Equiv m β ita itc

def Std.Iterators.IterM.Equiv {m : Type w → Type w'} [Monad m] [LawfulMonad m] {β α₁ α₂ : Type w} [Iterator α₁ m β] [Iterator α₂ m β] (ita : IterM m β) (itb : IterM m β) : Prop

Equivalence relation on monadic iterators. Equivalent iterators behave the same as long as the internal state of them is not directly inspected.

Two iterators (possibly of different types) are equivalent if they have the same Iterator.IsPlausibleStep relation and their step functions are the same up to equivalence of the successor iterators. This coinductive definition captures the idea that the only relevant feature of an iterator is its step function. Other information retrievable from the iterator -- for example, whether it is a list iterator or an array iterator -- is totally irrelevant for the equivalence judgement.

Equations

• ita.Equiv itb = Std.Iterators.BundledIterM.Equiv m β (Std.Iterators.BundledIterM.ofIterM ita) (Std.Iterators.BundledIterM.ofIterM itb)

def Std.Iterators.Iter.Equiv {α₁ α₂ β : Type u_1} [Iterator α₁ Id β] [Iterator α₂ Id β] (ita : Iter β) (itb : Iter β) : Prop

Equivalence relation on iterators. Equivalent iterators behave the same as long as the internal state of them is not directly inspected.

Two iterators (possibly of different types) are equivalent if they have the same Iterator.IsPlausibleStep relation and their step functions are the same up to equivalence of the successor iterators. This coinductive definition captures the idea that the only relevant feature of an iterator is its step function. Other information retrievable from the iterator -- for example, whether it is a list iterator or an array iterator -- is totally irrelevant for the equivalence judgement.

Equations

• ita.Equiv itb = ita.toIterM.Equiv itb.toIterM

theorem Std.Iterators.Iter.Equiv.toIterM {α₁ α₂ β : Type u_1} [Iterator α₁ Id β] [Iterator α₂ Id β] {ita : Iter β} {itb : Iter β} (h : ita.Equiv itb) : ita.toIterM.Equiv itb.toIterM

theorem Std.Iterators.IterM.Equiv.toIter {α₁ α₂ β : Type u_1} [Iterator α₁ Id β] [Iterator α₂ Id β] {ita : IterM Id β} {itb : IterM Id β} (h : ita.Equiv itb) : ita.toIter.Equiv itb.toIter

theorem Std.Iterators.IterM.Equiv.refl {m : Type w → Type w'} {β : Type w} [Monad m] [LawfulMonad m] {α : Type w} [Iterator α m β] (it : IterM m β) : it.Equiv it

theorem Std.Iterators.IterM.Equiv.symm {m : Type w → Type w'} {α₁ α₂ β : Type w} [Monad m] [LawfulMonad m] [Iterator α₁ m β] [Iterator α₂ m β] {ita : IterM m β} {itb : IterM m β} (h : ita.Equiv itb) : itb.Equiv ita

theorem Std.Iterators.IterM.Equiv.trans {m : Type w → Type w'} {α₁ α₂ α₃ β : Type w} [Monad m] [LawfulMonad m] [Iterator α₁ m β] [Iterator α₂ m β] [Iterator α₃ m β] {ita : IterM m β} {itb : IterM m β} {itc : IterM m β} (hab : ita.Equiv itb) (hbc : itb.Equiv itc) : ita.Equiv itc

theorem Std.Iterators.Iter.Equiv.refl {β α : Type w} [Iterator α Id β] (it : Iter β) : it.Equiv it

theorem Std.Iterators.Iter.Equiv.symm {α₁ α₂ β : Type w} [Iterator α₁ Id β] [Iterator α₂ Id β] {ita : Iter β} {itb : Iter β} (h : ita.Equiv itb) : itb.Equiv ita

theorem Std.Iterators.Iter.Equiv.trans {α₁ α₂ α₃ β : Type w} [Iterator α₁ Id β] [Iterator α₂ Id β] [Iterator α₃ Id β] {ita : Iter β} {itb : Iter β} {itc : Iter β} (hab : ita.Equiv itb) (hbc : itb.Equiv itc) : ita.Equiv itc

theorem Std.Iterators.IterM.Equiv.of_morphism {α₁ α₂ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {β : Type w} [Iterator α₁ m β] [Iterator α₂ m β] (ita : IterM m β) (f : IterM m β → IterM m β) (h : ∀ (it : IterM m β), (f it).stepAsHetT = IterStep.mapIterator f <$> it.stepAsHetT) : ita.Equiv (f ita)