@[unbox]

structure Std.Iterators.Types.Attach (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] (P : β → Prop) : Type w

Internal state of the attachWith combinator. Do not depend on its internals.

• inner : IterM m β
• invariant (out : β) : self.inner.IsPlausibleIndirectOutput out → P out

@[inline]

def Std.Iterators.Types.Attach.Monadic.modifyStep {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {P : β → Prop} (it : IterM m { out : β // P out }) (step : it.internalState.inner.Step) : IterStep (IterM m { out : β // P out }) { out : β // P out }

Equations

• Std.Iterators.Types.Attach.Monadic.modifyStep it ⟨Std.IterStep.yield it' out, h⟩ = Std.IterStep.yield { internalState := { inner := it', invariant := ⋯ } } ⟨out, ⋯⟩
• Std.Iterators.Types.Attach.Monadic.modifyStep it ⟨Std.IterStep.skip it', h⟩ = Std.IterStep.skip { internalState := { inner := it', invariant := ⋯ } }
• Std.Iterators.Types.Attach.Monadic.modifyStep it ⟨Std.IterStep.done, property⟩ = Std.IterStep.done

@[instance_reducible]

instance Std.Iterators.Types.Attach.instIterator {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] {P : β → Prop} : Iterator (Attach α m P) m { out : β // P out }

Equations

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

def Std.Iterators.Types.Attach.instFinitenessRelation {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Finite α m] {P : β → Prop} : FinitenessRelation (Attach α m P) m

Equations

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

instance Std.Iterators.Types.Attach.instFinite {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Finite α m] {P : β → Prop} : Finite (Attach α m P) m

def Std.Iterators.Types.Attach.instProductivenessRelation {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Productive α m] {P : β → Prop} : ProductivenessRelation (Attach α m P) m

Equations

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

instance Std.Iterators.Types.Attach.instProductive {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Productive α m] {P : β → Prop} : Productive (Attach α m P) m

@[instance_reducible]

instance Std.Iterators.Types.Attach.instIteratorLoop {α β : Type w} {m : Type w → Type w'} [Monad m] {n : Type x → Type x'} [Monad n] {P : β → Prop} [Iterator α m β] : IteratorLoop (Attach α m P) m n

Equations

• Std.Iterators.Types.Attach.instIteratorLoop = Std.IteratorLoop.defaultImplementation

@[inline]

def Std.IterM.attachWith {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] (it : IterM m β) (P : β → Prop) (h : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out) : IterM m { out : β // P out }

“Attaches” individual proofs to an iterator of values that satisfy a predicate P, returning an iterator with values in the corresponding subtype { x // P x }.

Termination properties:

• Finite instance: only if the base iterator is finite
• Productive instance: only if the base iterator is productive

Equations

• it.attachWith P h = { internalState := { inner := it, invariant := h } }