@[irreducible, specialize #[]]

def Std.Iterators.IterM.inductSteps {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Iterator α m β] [Finite α m] (motive : IterM m β → Sort x) (step : (it : IterM m β) → ({it' : IterM m β} → {out : β} → it.IsPlausibleStep (IterStep.yield it' out) → motive it') → ({it' : IterM m β} → it.IsPlausibleStep (IterStep.skip it') → motive it') → motive it) (it : IterM m β) : motive it

Induction principle for finite monadic 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.

@[irreducible, specialize #[]]

def Std.Iterators.IterM.inductSkips {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Iterator α m β] [Productive α m] (motive : IterM m β → Sort x) (step : (it : IterM m β) → ({it' : IterM m β} → it.IsPlausibleStep (IterStep.skip it') → motive it') → motive it) (it : IterM m β) : motive it

Induction principle for productive monadic 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

• Std.Iterators.IterM.inductSkips motive step it = step it fun {it' : Std.IterM m β} (x : it.IsPlausibleStep (Std.Iterators.IterStep.skip it')) => Std.Iterators.IterM.inductSkips motive step it'