source
theorem Std.Iterators.Iter.toArray_eq_toArray_toIterM {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} :
it.toArray = it.toIterM.toArray.run
source
theorem Std.Iterators.Iter.toList_eq_toList_toIterM {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} :
it.toList = it.toIterM.toList.run
source
theorem Std.Iterators.Iter.toListRev_eq_toListRev_toIterM {α β : Type u_1} [Iterator α Id β] [Finite α Id] {it : Iter β} :
it.toListRev = it.toIterM.toListRev.run
source
@[simp]
theorem Std.Iterators.IterM.toList_toIter {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] {it : IterM Id β} :
it.toIter.toList = it.toList.run
source
@[simp]
theorem Std.Iterators.IterM.toListRev_toIter {α β : Type u_1} [Iterator α Id β] [Finite α Id] {it : IterM Id β} :
it.toIter.toListRev = it.toListRev.run
source
@[simp]
theorem Std.Iterators.Iter.toList_toArray {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} :
it.toArray.toList = it.toList
source
@[simp]
theorem Std.Iterators.Iter.toArray_toList {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} :
it.toList.toArray = it.toArray
source
@[simp]
theorem Std.Iterators.Iter.reverse_toListRev {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} :
it.toListRev.reverse = it.toList
source
theorem Std.Iterators.Iter.toListRev_eq {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} :
it.toListRev = it.toList.reverse
source
theorem Std.Iterators.Iter.toArray_eq_match_step {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} :
it.toArray = match it.step.val with | IterStep.yield it' out => #[out] ++ it'.toArray | IterStep.skip it' => it'.toArray | IterStep.done => #[]
source
theorem Std.Iterators.Iter.toList_eq_match_step {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} :
it.toList = match it.step.val with | IterStep.yield it' out => out :: it'.toList | IterStep.skip it' => it'.toList | IterStep.done => []
source
theorem Std.Iterators.Iter.toListRev_eq_match_step {α β : Type u_1} [Iterator α Id β] [Finite α Id] {it : Iter β} :
it.toListRev = match it.step.val with | IterStep.yield it' out => it'.toListRev ++ [out] | IterStep.skip it' => it'.toListRev | IterStep.done => []
source
theorem Std.Iterators.Iter.getElem?_toList_eq_atIdxSlow? {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} {k : Nat} :
it.toList[k]? = atIdxSlow? k it
source
theorem Std.Iterators.Iter.toList_eq_of_atIdxSlow?_eq {α₁ α₂ β : Type u_1} [Iterator α₁ Id β] [Finite α₁ Id] [IteratorCollect α₁ Id Id] [LawfulIteratorCollect α₁ Id Id] [Iterator α₂ Id β] [Finite α₂ Id] [IteratorCollect α₂ Id Id] [LawfulIteratorCollect α₂ Id Id] {it₁ : Iter β} {it₂ : Iter β} (h : ∀ (k : Nat), atIdxSlow? k it₁ = atIdxSlow? k it₂) :
it₁.toList = it₂.toList
source
theorem Std.Iterators.Iter.isPlausibleIndirectOutput_of_mem_toList {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} {b : β} :
b ∈ it.toList → it.IsPlausibleIndirectOutput b
source
theorem Std.Iterators.Iter.isPlausibleIndirectOutput_of_mem_toListRev {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} {b : β} :
b ∈ it.toListRev → it.IsPlausibleIndirectOutput b
source
theorem Std.Iterators.Iter.isPlausibleIndirectOutput_of_mem_toArray {α β : Type u_1} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} {b : β} :
b ∈ it.toArray → it.IsPlausibleIndirectOutput b