@[inline]

def Std.Iter.append {α₁ α₂ β : Type w} [Iterator α₁ Id β] [Iterator α₂ Id β] (it₁ : Iter β) (it₂ : Iter β) : Iter β

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₂ = (it₁.toIterM.append it₂.toIterM).toIter

@[inline]

def Std.Iter.Intermediate.appendSnd {α₂ β : Type w} [Iterator α₂ Id β] (α₁ : Type w) (it₂ : Iter β) : Iter β

This combinator is only useful for advanced use cases.

Given an iterator it₂, returns an iterator that behaves exactly like it₂ but is of 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--⊥
Iter.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 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₂.

Equations

• Std.Iter.Intermediate.appendSnd α₁ it₂ = (Std.IterM.Intermediate.appendSnd α₁ it₂.toIterM).toIter