@[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
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'.