Documentation

Std.Data.Iterators.Lemmas.Consumers.Loop

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) :
forIn ita init f = forIn itb init f
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) :
foldM f init ita = foldM f init 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) :
fold f init ita = fold f init itb