Documentation

Std.Data.Iterators.Lemmas.Basic

@[irreducible, specialize #[]]
def Std.Iterators.Iter.inductSteps {α β : Type u_1} [Iterator α Id β] [Finite α Id] (motive : Iter βSort x) (step : (it : Iter β) → ({it' : Iter β} → {out : β} → it.IsPlausibleStep (IterStep.yield it' out)motive it')({it' : Iter β} → it.IsPlausibleStep (IterStep.skip it')motive it')motive it) (it : Iter β) :
motive it

Induction principle for finite iterators: One can define a function f that maps every iterator it to an element of motive it by defining f it in terms of the values of f on the plausible successors of `it'.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[irreducible, specialize #[]]
    def Std.Iterators.Iter.inductSkips {α β : Type u_1} [Iterator α Id β] [Productive α Id] (motive : Iter βSort x) (step : (it : Iter β) → ({it' : Iter β} → it.IsPlausibleStep (IterStep.skip it')motive it')motive it) (it : Iter β) :
    motive it

    Induction principle for productive iterators: One can define a function f that maps every iterator it to an element of motive it by defining f it in terms of the values of f on the plausible skip successors of `it'.

    Equations
    Instances For