This is an internal module used by iterator implementations.

structure Std.Iterators.FinitenessRelation (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] : Type w

Internal implementation detail of the iterator library. The purpose of this class is that it implies a Finite instance but it is more convenient to implement.

• rel : IterM m β → IterM m β → Prop
• wf : WellFounded self.rel
• subrelation {it it' : IterM m β} : it'.IsPlausibleSuccessorOf it → self.rel it' it

theorem Std.Iterators.Finite.of_finitenessRelation {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] (r : FinitenessRelation α m) : Finite α m

structure Std.Iterators.ProductivenessRelation (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] : Type w

Internal implementation detail of the iterator library. The purpose of this class is that it implies a Productive instance but it is more convenient to implement.

• rel : IterM m β → IterM m β → Prop
• wf : WellFounded self.rel
• subrelation {it it' : IterM m β} : it'.IsPlausibleSkipSuccessorOf it → self.rel it' it

theorem Std.Iterators.Productive.of_productivenessRelation {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] (r : ProductivenessRelation α m) : Productive α m