@[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
- Std.Iterators.Iter.inductSkips motive step it = step it fun {it' : Std.Iter β} (x : it.IsPlausibleStep (Std.Iterators.IterStep.skip it')) => Std.Iterators.Iter.inductSkips motive step it'