theorem
Std.Slice.Internal.iter_eq_toIteratorIter
{β : Type v}
{γ : Type u}
{s : Slice γ}
[Iterators.ToIterator s Id β]
:
theorem
Std.Slice.Internal.size_eq_size_iter
{γ : Type u}
{β : Type v}
{s : Slice γ}
[Iterators.ToIterator s Id β]
[Iterators.Iterator (Iterators.ToIterator.State s Id) Id β]
[Iterators.IteratorSize (Iterators.ToIterator.State s Id) Id]
:
theorem
Std.Slice.Internal.toArray_eq_toArray_iter
{γ : Type u}
{β : Type v}
{s : Slice γ}
[Iterators.ToIterator s Id β]
[Iterators.Iterator (Iterators.ToIterator.State s Id) Id β]
[Iterators.IteratorCollect (Iterators.ToIterator.State s Id) Id Id]
[Iterators.Finite (Iterators.ToIterator.State s Id) Id]
:
theorem
Std.Slice.Internal.toList_eq_toList_iter
{γ : Type u}
{β : Type v}
{s : Slice γ}
[Iterators.ToIterator s Id β]
[Iterators.Iterator (Iterators.ToIterator.State s Id) Id β]
[Iterators.IteratorCollect (Iterators.ToIterator.State s Id) Id Id]
[Iterators.Finite (Iterators.ToIterator.State s Id) Id]
:
theorem
Std.Slice.Internal.toListRev_eq_toListRev_iter
{γ : Type u}
{β : Type v}
{s : Slice γ}
[Iterators.ToIterator s Id β]
[Iterators.Iterator (Iterators.ToIterator.State s Id) Id β]
[Iterators.Finite (Iterators.ToIterator.State s Id) Id]
:
@[simp]
theorem
Std.Slice.size_toArray_eq_size
{γ : Type u}
{β : Type v}
{s : Slice γ}
[Iterators.ToIterator s Id β]
[Iterators.Iterator (Iterators.ToIterator.State s Id) Id β]
[Iterators.IteratorSize (Iterators.ToIterator.State s Id) Id]
[Iterators.IteratorCollect (Iterators.ToIterator.State s Id) Id Id]
[Iterators.Finite (Iterators.ToIterator.State s Id) Id]
[Iterators.LawfulIteratorSize (Iterators.ToIterator.State s Id)]
[Iterators.LawfulIteratorCollect (Iterators.ToIterator.State s Id) Id Id]
:
@[simp]
theorem
Std.Slice.length_toList_eq_size
{γ : Type u}
{β : Type v}
{s : Slice γ}
[Iterators.ToIterator s Id β]
[Iterators.Iterator (Iterators.ToIterator.State s Id) Id β]
[Iterators.IteratorSize (Iterators.ToIterator.State s Id) Id]
[Iterators.IteratorCollect (Iterators.ToIterator.State s Id) Id Id]
[Iterators.Finite (Iterators.ToIterator.State s Id) Id]
[Iterators.LawfulIteratorSize (Iterators.ToIterator.State s Id)]
[Iterators.LawfulIteratorCollect (Iterators.ToIterator.State s Id) Id Id]
:
@[simp]
theorem
Std.Slice.length_toListRev_eq_size
{γ : Type u}
{β : Type v}
{s : Slice γ}
[Iterators.ToIterator s Id β]
[Iterators.Iterator (Iterators.ToIterator.State s Id) Id β]
[Iterators.IteratorSize (Iterators.ToIterator.State s Id) Id]
[Iterators.IteratorCollect (Iterators.ToIterator.State s Id) Id Id]
[Iterators.Finite (Iterators.ToIterator.State s Id) Id]
[Iterators.LawfulIteratorSize (Iterators.ToIterator.State s Id)]
[Iterators.LawfulIteratorCollect (Iterators.ToIterator.State s Id) Id Id]
: