This module provides the iterator combinator IterM.append.

inductive Std.Iterators.Types.Append (α₁ α₂ : Type w) (m : Type w → Type w') (β : Type w) : Type w

The internal state of the IterM.append iterator combinator.

• fst {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} : IterM m β → IterM m β → Append α₁ α₂ m β
• snd {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} : IterM m β → Append α₁ α₂ m β

@[inline]

def Std.IterM.append {m : Type w → Type w'} {β α₁ α₂ : Type w} [Iterator α₁ m β] [Iterator α₂ m β] (it₁ : IterM m β) (it₂ : IterM m β) : IterM m β

Given two iterators it₁ and it₂, it₁.append it₂ is an iterator that first outputs all values of it₁ in order and then all values of it₂ in order.

Marble diagram:

it₁                 ---a----b---c--⊥
it₂                                 --d--e--⊥
it₁.append it₂      ---a----b---c-----d--e--⊥

Termination properties:

• Finite instance: only if it₁ and it₂ are finite
• Productive instance: only if it₁ and it₂ are productive

Note: If it₁ is not finite, then it₁.append it₂ can be productive while it₂ is not. The standard library does not provide a Productive instance for this case.

Performance:

This combinator incurs an additional O(1) cost with each output of it₁ and it₂.

Equations

• it₁.append it₂ = { internalState := Std.Iterators.Types.Append.fst it₁ it₂ }

@[inline]

def Std.IterM.Intermediate.appendSnd {m : Type w → Type w'} {β α₂ : Type w} [Iterator α₂ m β] (α₁ : Type w) (it₂ : IterM m β) : IterM m β

This combinator is only useful for advanced use cases.

Given an iterator it₂, IterM.Intermediate.appendSnd α₁ it₂ returns an iterator that behaves exactly like it₂ but has the same type as it₁.append it₂ (after it₁ has been exhausted). This is useful for constructing intermediate states of the append iterator.

Marble diagram:

it₂                                  --a--b--⊥
IterM.Intermediate.appendSnd α₁ it₂  --a--b--⊥

Termination properties:

• Finite instance: only if it₂ and iterators of type α₁ are finite
• Productive instance: only if it₂ and iterators of type α₁ are productive

Note: If iterators of type α₁ are not finite, then appendSnd α₁ it₂ can be productive while it₂ is not. The standard library does not provide a Productive instance for this case.

Performance:

This combinator incurs an additional O(1) cost with each output of it₂.

Equations

• Std.IterM.Intermediate.appendSnd α₁ it₂ = { internalState := Std.Iterators.Types.Append.snd it₂ }

inductive Std.Iterators.Types.Append.PlausibleStep {m : Type w → Type w'} {β α₁ α₂ : Type w} [Iterator α₁ m β] [Iterator α₂ m β] : IterM m β → IterStep (IterM m β) β → Prop

• fstYield {m : Type w → Type w'} {β α₁ α₂ : Type w} [Iterator α₁ m β] [Iterator α₂ m β] {it₁' : IterM m β} {out : β} {it₁ : IterM m β} {it₂ : IterM m β} : it₁.IsPlausibleStep (IterStep.yield it₁' out) → PlausibleStep (it₁.append it₂) (IterStep.yield (it₁'.append it₂) out)
• fstSkip {m : Type w → Type w'} {β α₁ α₂ : Type w} [Iterator α₁ m β] [Iterator α₂ m β] {it₁' it₁ : IterM m β} {it₂ : IterM m β} : it₁.IsPlausibleStep (IterStep.skip it₁') → PlausibleStep (it₁.append it₂) (IterStep.skip (it₁'.append it₂))
• fstDone {m : Type w → Type w'} {β α₁ α₂ : Type w} [Iterator α₁ m β] [Iterator α₂ m β] {it₁ : IterM m β} {it₂ : IterM m β} : it₁.IsPlausibleStep IterStep.done → PlausibleStep (it₁.append it₂) (IterStep.skip (IterM.Intermediate.appendSnd α₁ it₂))
• sndYield {m : Type w → Type w'} {β α₁ α₂ : Type w} [Iterator α₁ m β] [Iterator α₂ m β] {it₂' : IterM m β} {out : β} {it₂ : IterM m β} : it₂.IsPlausibleStep (IterStep.yield it₂' out) → PlausibleStep (IterM.Intermediate.appendSnd α₁ it₂) (IterStep.yield (IterM.Intermediate.appendSnd α₁ it₂') out)
• sndSkip {m : Type w → Type w'} {β α₁ α₂ : Type w} [Iterator α₁ m β] [Iterator α₂ m β] {it₂' it₂ : IterM m β} : it₂.IsPlausibleStep (IterStep.skip it₂') → PlausibleStep (IterM.Intermediate.appendSnd α₁ it₂) (IterStep.skip (IterM.Intermediate.appendSnd α₁ it₂'))
• sndDone {m : Type w → Type w'} {β α₁ α₂ : Type w} [Iterator α₁ m β] [Iterator α₂ m β] {it₂ : IterM m β} : it₂.IsPlausibleStep IterStep.done → PlausibleStep (IterM.Intermediate.appendSnd α₁ it₂) IterStep.done

@[implicit_reducible, inline]

instance Std.Iterators.Types.Append.instIterator {m : Type w → Type w'} {β α₁ α₂ : Type w} [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] : Iterator (Append α₁ α₂ m β) m β

Equations

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

@[implicit_reducible]

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

Equations

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

def Std.Iterators.Types.Append.Rel (α₁ α₂ : Type w) (m : Type w → Type w') (β : Type w) [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m] : IterM m β → IterM m β → Prop

Equations

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

theorem Std.Iterators.Types.Append.rel_of_fst {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m] {it₁ it₁' : IterM m β} {it₂ : IterM m β} (h : it₁'.finitelyManySteps.Rel it₁.finitelyManySteps) : Rel α₁ α₂ m β (it₁'.append it₂) (it₁.append it₂)

theorem Std.Iterators.Types.Append.rel_fstDone {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m] {it₁ : IterM m β} {it₂ : IterM m β} : Rel α₁ α₂ m β (IterM.Intermediate.appendSnd α₁ it₂) (it₁.append it₂)

theorem Std.Iterators.Types.Append.rel_of_snd {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m] {it₂ it₂' : IterM m β} (h : it₂'.finitelyManySteps.Rel it₂.finitelyManySteps) : Rel α₁ α₂ m β (IterM.Intermediate.appendSnd α₁ it₂') (IterM.Intermediate.appendSnd α₁ it₂)

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

Equations

• Std.Iterators.Types.Append.instFinitenessRelation = { Rel := Std.Iterators.Types.Append.Rel α₁ α₂ m β, wf := ⋯, subrelation := ⋯ }

instance Std.Iterators.Types.Append.instFinite {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m] : Finite (Append α₁ α₂ m β) m

def Std.Iterators.Types.Append.ProductiveRel (α₁ α₂ : Type w) (m : Type w → Type w') (β : Type w) [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] [Productive α₁ m] [Productive α₂ m] : IterM m β → IterM m β → Prop

Equations

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

theorem Std.Iterators.Types.Append.productiveRel_of_fst {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] [Productive α₁ m] [Productive α₂ m] {it₁ it₁' : IterM m β} {it₂ : IterM m β} (h : it₁'.finitelyManySkips.Rel it₁.finitelyManySkips) : ProductiveRel α₁ α₂ m β (it₁'.append it₂) (it₁.append it₂)

theorem Std.Iterators.Types.Append.productiveRel_fstDone {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] [Productive α₁ m] [Productive α₂ m] {it₁ : IterM m β} {it₂ : IterM m β} : ProductiveRel α₁ α₂ m β (IterM.Intermediate.appendSnd α₁ it₂) (it₁.append it₂)

theorem Std.Iterators.Types.Append.productiveRel_of_snd {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] [Productive α₁ m] [Productive α₂ m] {it₂ it₂' : IterM m β} (h : it₂'.finitelyManySkips.Rel it₂.finitelyManySkips) : ProductiveRel α₁ α₂ m β (IterM.Intermediate.appendSnd α₁ it₂') (IterM.Intermediate.appendSnd α₁ it₂)

instance Std.Iterators.Types.Append.instProductive {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] [Productive α₁ m] [Productive α₂ m] : Productive (Append α₁ α₂ m β) m