theorem
Std.Iterators.Iter.Equiv.forIn_eq
{α₁ α₂ β γ : Type w}
{m : Type w → Type w'}
[Iterator α₁ Id β]
[Iterator α₂ Id β]
[Finite α₁ Id]
[Finite α₂ Id]
[Monad m]
[LawfulMonad m]
[IteratorLoop α₁ Id m]
[LawfulIteratorLoop α₁ Id m]
[IteratorLoop α₂ Id m]
[LawfulIteratorLoop α₂ Id m]
{init : γ}
{f : β → γ → m (ForInStep γ)}
{ita : Iter β}
{itb : Iter β}
(h : ita.Equiv itb)
:
theorem
Std.Iterators.Iter.Equiv.foldM_eq
{α₁ α₂ β γ : Type w}
{m : Type w → Type w'}
[Iterator α₁ Id β]
[Iterator α₂ Id β]
[Iterator α₁ Id β]
[Iterator α₂ Id β]
[Finite α₁ Id]
[Finite α₂ Id]
[Monad m]
[LawfulMonad m]
[IteratorLoop α₁ Id m]
[LawfulIteratorLoop α₁ Id m]
[IteratorLoop α₂ Id m]
[LawfulIteratorLoop α₂ Id m]
{init : γ}
{f : γ → β → m γ}
{ita : Iter β}
{itb : Iter β}
(h : ita.Equiv itb)
:
theorem
Std.Iterators.Iter.Equiv.fold_eq
{α₁ α₂ β γ : Type w}
{m : Type w → Type w'}
[Iterator α₁ Id β]
[Iterator α₂ Id β]
[Iterator α₁ Id β]
[Iterator α₂ Id β]
[Finite α₁ Id]
[Finite α₂ Id]
[Monad m]
[LawfulMonad m]
[IteratorLoop α₁ Id Id]
[LawfulIteratorLoop α₁ Id Id]
[IteratorLoop α₂ Id Id]
[LawfulIteratorLoop α₂ Id Id]
{init : γ}
{f : γ → β → γ}
{ita : Iter β}
{itb : Iter β}
(h : ita.Equiv itb)
: