This is an internal module used by iterator implementations.

source
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

Instances For

source
theorem Std.Iterators.Finite.of_finitenessRelation {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] (r : FinitenessRelation α m) :
Finite α m
source
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

Instances For

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