Documentation

Std.Data.Iterators.Internal.Termination

This is an internal module used by iterator implementations.

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

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.

Instances For
    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 β] :

    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.

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