Slices of USizeArray

Slices of USizeArray: the type, reads, slice notation, iterators, folds and searches, membership and equality, and collecting iterators into arrays.

The slice type

structure ScalarArray.USizeArray.SliceData : Type

Internal representation of USizeArray.Slice.

• array : USizeArray

  The underlying array.

• start : Nat

  The starting index of the slice (inclusive).

• stop : Nat

  The ending index of the slice (exclusive).

• start_le_stop : self.start ≤ self.stop

  The starting index is no later than the ending index.

• stop_le_array_size : self.stop ≤ self.array.size

  The ending index is no later than the end of the array.

@[reducible, inline]

abbrev ScalarArray.USizeArray.Slice : Type

A region of a USizeArray: the elements from index start up to, but not including, stop. Taking a slice doesn't copy the array. Slices are written with core's slice notation, such as a[i...j], a[i...*] or a[*...j].

Equations

• ScalarArray.USizeArray.Slice = Std.Slice ScalarArray.USizeArray.SliceData

instance ScalarArray.USizeArray.instSelfSliceSliceDataSlice : Std.Slice.Self (Std.Slice USizeArray.SliceData) USizeArray.Slice

@[inline]

def ScalarArray.USizeArray.Slice.array (s : USizeArray.Slice) : USizeArray

The underlying array.

Equations

• s.array = s.internalRepresentation.array

@[inline]

def ScalarArray.USizeArray.Slice.start (s : USizeArray.Slice) : Nat

The starting index of the slice (inclusive).

Equations

• s.start = s.internalRepresentation.start

@[inline]

def ScalarArray.USizeArray.Slice.stop (s : USizeArray.Slice) : Nat

The ending index of the slice (exclusive).

Equations

• s.stop = s.internalRepresentation.stop

theorem ScalarArray.USizeArray.Slice.start_le_stop (s : USizeArray.Slice) : s.start ≤ s.stop

The starting index is no later than the ending index.

theorem ScalarArray.USizeArray.Slice.stop_le_array_size (s : USizeArray.Slice) : s.stop ≤ s.array.size

The ending index is no later than the end of the array.

@[instance_reducible]

instance ScalarArray.USizeArray.Slice.instSliceSizeSliceData : Std.Slice.SliceSize USizeArray.SliceData

Equations

• ScalarArray.USizeArray.Slice.instSliceSizeSliceData = { size := fun (s : Std.Slice ScalarArray.USizeArray.SliceData) => s.internalRepresentation.stop - s.internalRepresentation.start }

theorem ScalarArray.USizeArray.Slice.size_eq (s : USizeArray.Slice) : Std.Slice.size s = s.stop - s.start

Reads

@[inline]

def ScalarArray.USizeArray.Slice.get (s : USizeArray.Slice) (i : Nat) (h : i < Std.Slice.size s := by get_elem_tactic) : USize

The element at index i of the slice, counted from the start of the slice.

Equations

• s.get i h = s.array[s.start + i]

@[instance_reducible]

instance ScalarArray.USizeArray.Slice.instGetElemNatUSizeLtSizeSliceData : GetElem USizeArray.Slice Nat USize fun (s : USizeArray.Slice) (i : Nat) => i < Std.Slice.size s

Equations

• ScalarArray.USizeArray.Slice.instGetElemNatUSizeLtSizeSliceData = { getElem := fun (s : ScalarArray.USizeArray.Slice) (i : Nat) (h : i < Std.Slice.size s) => s.get i h }

@[inline]

def ScalarArray.USizeArray.Slice.getD (s : USizeArray.Slice) (i : Nat) (v₀ : USize) : USize

The element at index i of the slice, or v₀ if i is out of bounds.

Equations

• s.getD i v₀ = if h : i < Std.Slice.size s then s[i] else v₀

@[reducible, inline]

abbrev ScalarArray.USizeArray.Slice.get! (s : USizeArray.Slice) (i : Nat) : USize

The element at index i of the slice, or default if i is out of bounds.

Equations

• s.get! i = s.getD i default

@[inline]

def ScalarArray.USizeArray.Slice.popFront (s : USizeArray.Slice) : USizeArray.Slice

Removes the first element of the slice, if any.

Equations

• One or more equations did not get rendered due to their size.

The empty slice, copies and printing

def ScalarArray.USizeArray.Slice.empty : USizeArray.Slice

The empty slice, backed by an empty array.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance ScalarArray.USizeArray.Slice.instEmptyCollection : EmptyCollection USizeArray.Slice

Equations

• ScalarArray.USizeArray.Slice.instEmptyCollection = { emptyCollection := ScalarArray.USizeArray.Slice.empty }

@[instance_reducible]

instance ScalarArray.USizeArray.Slice.instInhabited : Inhabited USizeArray.Slice

Equations

• ScalarArray.USizeArray.Slice.instInhabited = { default := ScalarArray.USizeArray.Slice.empty }

def ScalarArray.USizeArray.Slice.copy (s : USizeArray.Slice) : USizeArray

The elements of the slice, copied into a new array with a single memmove.

Equations

• s.copy = s.array.extract s.start s.stop

theorem ScalarArray.USizeArray.Slice.getElem_eq (s : USizeArray.Slice) (i : Nat) (h : i < Std.Slice.size s) : s[i] = s.array[s.start + i]

@[instance_reducible]

instance ScalarArray.USizeArray.Slice.instRepr : Repr USizeArray.Slice

Prints the array and the bounds in slice notation, (ScalarArray.USizeArray.mk #[...])[i...j], which evaluates to an equal slice: slices are equal when their arrays and bounds are.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance ScalarArray.USizeArray.Slice.instToString : ToString USizeArray.Slice

Equations

• ScalarArray.USizeArray.Slice.instToString = { toString := fun (s : ScalarArray.USizeArray.Slice) => toString s.copy }

Slice notation

@[inline]

def ScalarArray.USizeArray.toSlice (a : USizeArray) (start : Nat := 0) (stop : Nat := a.size) : USizeArray.Slice

The slice of a from index start up to, but not including, stop. If start or stop are not valid bounds, they are clamped to the size of a, and start is clamped to stop.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance ScalarArray.USizeArray.instCoeSlice : Coe USizeArray USizeArray.Slice

Arrays coerce to slices, which is free. Slices don't coerce back, since that copies.

Equations

• ScalarArray.USizeArray.instCoeSlice = { coe := fun (x : ScalarArray.USizeArray) => x.toSlice }

@[instance_reducible]

instance ScalarArray.USizeArray.instSliceableNatSlice : Std.Rcc.Sliceable USizeArray Nat USizeArray.Slice

Equations

• ScalarArray.USizeArray.instSliceableNatSlice = { mkSlice := fun (a : ScalarArray.USizeArray) (range : Std.Rcc Nat) => a.toSlice range.lower (range.upper + 1) }

@[instance_reducible]

instance ScalarArray.USizeArray.instSliceableNatSlice_1 : Std.Rco.Sliceable USizeArray Nat USizeArray.Slice

Equations

• ScalarArray.USizeArray.instSliceableNatSlice_1 = { mkSlice := fun (a : ScalarArray.USizeArray) (range : Std.Rco Nat) => a.toSlice range.lower range.upper }

@[instance_reducible]

instance ScalarArray.USizeArray.instSliceableNatSlice_2 : Std.Rci.Sliceable USizeArray Nat USizeArray.Slice

Equations

• ScalarArray.USizeArray.instSliceableNatSlice_2 = { mkSlice := fun (a : ScalarArray.USizeArray) (range : Std.Rci Nat) => a.toSlice range.lower }

@[instance_reducible]

instance ScalarArray.USizeArray.instSliceableNatSlice_3 : Std.Roc.Sliceable USizeArray Nat USizeArray.Slice

Equations

• ScalarArray.USizeArray.instSliceableNatSlice_3 = { mkSlice := fun (a : ScalarArray.USizeArray) (range : Std.Roc Nat) => a.toSlice (range.lower + 1) (range.upper + 1) }

@[instance_reducible]

instance ScalarArray.USizeArray.instSliceableNatSlice_4 : Std.Roo.Sliceable USizeArray Nat USizeArray.Slice

Equations

• ScalarArray.USizeArray.instSliceableNatSlice_4 = { mkSlice := fun (a : ScalarArray.USizeArray) (range : Std.Roo Nat) => a.toSlice (range.lower + 1) range.upper }

@[instance_reducible]

instance ScalarArray.USizeArray.instSliceableNatSlice_5 : Std.Roi.Sliceable USizeArray Nat USizeArray.Slice

Equations

• ScalarArray.USizeArray.instSliceableNatSlice_5 = { mkSlice := fun (a : ScalarArray.USizeArray) (range : Std.Roi Nat) => a.toSlice (range.lower + 1) }

@[instance_reducible]

instance ScalarArray.USizeArray.instSliceableNatSlice_6 : Std.Ric.Sliceable USizeArray Nat USizeArray.Slice

Equations

• ScalarArray.USizeArray.instSliceableNatSlice_6 = { mkSlice := fun (a : ScalarArray.USizeArray) (range : Std.Ric Nat) => a.toSlice 0 (range.upper + 1) }

@[instance_reducible]

instance ScalarArray.USizeArray.instSliceableNatSlice_7 : Std.Rio.Sliceable USizeArray Nat USizeArray.Slice

Equations

• ScalarArray.USizeArray.instSliceableNatSlice_7 = { mkSlice := fun (a : ScalarArray.USizeArray) (range : Std.Rio Nat) => a.toSlice 0 range.upper }

@[instance_reducible]

instance ScalarArray.USizeArray.instSliceableNatSlice_8 : Std.Rii.Sliceable USizeArray Nat USizeArray.Slice

Equations

• ScalarArray.USizeArray.instSliceableNatSlice_8 = { mkSlice := fun (a : ScalarArray.USizeArray) (x : Std.Rii Nat) => a.toSlice }

@[inline]

def ScalarArray.USizeArray.Slice.slice (s : USizeArray.Slice) (start : Nat := 0) (stop : Nat := Std.Slice.size s) : USizeArray.Slice

The slice of s from index start up to, but not including, stop, clamped like toSlice.

Equations

• s.slice start stop = s.array.toSlice (s.start + min start (Std.Slice.size s)) (s.start + min stop (Std.Slice.size s))

@[instance_reducible]

instance ScalarArray.USizeArray.instSliceableSliceNat : Std.Rcc.Sliceable USizeArray.Slice Nat USizeArray.Slice

Equations

• ScalarArray.USizeArray.instSliceableSliceNat = { mkSlice := fun (s : ScalarArray.USizeArray.Slice) (range : Std.Rcc Nat) => s.slice range.lower (range.upper + 1) }

@[instance_reducible]

instance ScalarArray.USizeArray.instSliceableSliceNat_1 : Std.Rco.Sliceable USizeArray.Slice Nat USizeArray.Slice

Equations

• ScalarArray.USizeArray.instSliceableSliceNat_1 = { mkSlice := fun (s : ScalarArray.USizeArray.Slice) (range : Std.Rco Nat) => s.slice range.lower range.upper }

@[instance_reducible]

instance ScalarArray.USizeArray.instSliceableSliceNat_2 : Std.Rci.Sliceable USizeArray.Slice Nat USizeArray.Slice

Equations

• ScalarArray.USizeArray.instSliceableSliceNat_2 = { mkSlice := fun (s : ScalarArray.USizeArray.Slice) (range : Std.Rci Nat) => s.slice range.lower }

@[instance_reducible]

instance ScalarArray.USizeArray.instSliceableSliceNat_3 : Std.Roc.Sliceable USizeArray.Slice Nat USizeArray.Slice

Equations

• ScalarArray.USizeArray.instSliceableSliceNat_3 = { mkSlice := fun (s : ScalarArray.USizeArray.Slice) (range : Std.Roc Nat) => s.slice (range.lower + 1) (range.upper + 1) }

@[instance_reducible]

instance ScalarArray.USizeArray.instSliceableSliceNat_4 : Std.Roo.Sliceable USizeArray.Slice Nat USizeArray.Slice

Equations

• ScalarArray.USizeArray.instSliceableSliceNat_4 = { mkSlice := fun (s : ScalarArray.USizeArray.Slice) (range : Std.Roo Nat) => s.slice (range.lower + 1) range.upper }

@[instance_reducible]

instance ScalarArray.USizeArray.instSliceableSliceNat_5 : Std.Roi.Sliceable USizeArray.Slice Nat USizeArray.Slice

Equations

• ScalarArray.USizeArray.instSliceableSliceNat_5 = { mkSlice := fun (s : ScalarArray.USizeArray.Slice) (range : Std.Roi Nat) => s.slice (range.lower + 1) }

@[instance_reducible]

instance ScalarArray.USizeArray.instSliceableSliceNat_6 : Std.Ric.Sliceable USizeArray.Slice Nat USizeArray.Slice

Equations

• ScalarArray.USizeArray.instSliceableSliceNat_6 = { mkSlice := fun (s : ScalarArray.USizeArray.Slice) (range : Std.Ric Nat) => s.slice 0 (range.upper + 1) }

@[instance_reducible]

instance ScalarArray.USizeArray.instSliceableSliceNat_7 : Std.Rio.Sliceable USizeArray.Slice Nat USizeArray.Slice

Equations

• ScalarArray.USizeArray.instSliceableSliceNat_7 = { mkSlice := fun (s : ScalarArray.USizeArray.Slice) (range : Std.Rio Nat) => s.slice 0 range.upper }

@[instance_reducible]

instance ScalarArray.USizeArray.instSliceableSliceNat_8 : Std.Rii.Sliceable USizeArray.Slice Nat USizeArray.Slice

Equations

• ScalarArray.USizeArray.instSliceableSliceNat_8 = { mkSlice := fun (s : ScalarArray.USizeArray.Slice) (x : Std.Rii Nat) => s }

Iterators

structure ScalarArray.USizeArray.SliceIterator : Type

The iterator over the elements of a slice, used for for loops and the generic slice API.

• xs : USizeArray.Slice

  The rest of the slice.

@[inline]

def ScalarArray.USizeArray.SliceIterator.step {m : Type → Type u_1} : Std.IterM Id USize → Std.IterStep (Std.IterM m USize) USize

One step of the iterator: the first element of the rest of the slice, if there is one.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance ScalarArray.USizeArray.instIteratorSliceIteratorIdUSize : Std.Iterator USizeArray.SliceIterator Id USize

Equations

• One or more equations did not get rendered due to their size.

instance ScalarArray.USizeArray.instFiniteSliceIteratorIdUSize : Std.Iterators.Finite USizeArray.SliceIterator Id

@[implemented_by _private.ScalarArray.USize.Slice.0.ScalarArray.USizeArray.SliceIterator.forInImpl]

def ScalarArray.USizeArray.SliceIterator.forIn {n : Type x → Type x'} [Monad n] (lift : (γ : Type) → (δ : Type x) → (γ → n δ) → Id γ → n δ) (γ : Type x) (Pl : USize → γ → ForInStep γ → Prop) (it : Std.IterM Id USize) (init : γ) (f : (b : USize) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) : n γ

The loop behind for loops and the Std.Iterators consumers on slices. Logically it is Std.IteratorLoop.defaultImplementation, which steps the iterator one element at a time; it is implemented by a loop over the USize indices of the underlying array.

Equations

• ScalarArray.USizeArray.SliceIterator.forIn lift γ Pl it init f = Std.IteratorLoop.forIn lift γ Pl it init f

@[instance_reducible]

instance ScalarArray.USizeArray.instIteratorLoopSliceIteratorIdUSizeOfMonad {m : Type u_1 → Type u_2} [Monad m] : Std.IteratorLoop USizeArray.SliceIterator Id m

Equations

• ScalarArray.USizeArray.instIteratorLoopSliceIteratorIdUSizeOfMonad = { forIn := ScalarArray.USizeArray.SliceIterator.forIn }

instance ScalarArray.USizeArray.instLawfulIteratorLoopUSizeSliceIteratorId {m : Type u_1 → Type u_2} [Monad m] : Std.LawfulIteratorLoop USizeArray.SliceIterator Id m

@[instance_reducible]

instance ScalarArray.USizeArray.instToIteratorSliceSliceDataIdSliceIteratorUSize : Std.ToIterator (Std.Slice USizeArray.SliceData) Id USizeArray.SliceIterator USize

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance ScalarArray.USizeArray.instForInSliceUSizeOfMonad {m : Type u_1 → Type u_2} [Monad m] : ForIn m USizeArray.Slice USize

Equations

• ScalarArray.USizeArray.instForInSliceUSizeOfMonad = inferInstance

@[instance_reducible]

instance ScalarArray.USizeArray.instForMSliceUSizeOfMonad {m : Type u_1 → Type u_2} [Monad m] : ForM m USizeArray.Slice USize

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.Iter.toUSizeSlice (it : Iter USize) : ScalarArray.USizeArray.Slice

The elements that the slice iterator it has yet to yield, as a slice of the same array, without copying. The start of the slice is the index of the next element in the array.

Equations

• it.toUSizeSlice = it.internalState.xs

@[inline]

def ScalarArray.USizeArray.iter (a : USizeArray) : Std.Iter USize

An iterator over the elements of a, for use with the Std.Iterators API.

Equations

• a.iter = Std.Slice.iter a.toSlice

Folds and searches

def ScalarArray.USizeArray.Slice.foldrM {β : Type v} {m : Type v → Type w} [Monad m] (f : USize → β → m β) (init : β) (s : USizeArray.Slice) : m β

Folds a monadic function over the elements of s, from last to first.

Equations

• ScalarArray.USizeArray.Slice.foldrM f init s = ScalarArray.USizeArray.Slice.foldrM.loop f s (Std.Slice.size s) ⋯ init

@[specialize #[]]

def ScalarArray.USizeArray.Slice.foldrM.loop {β : Type v} {m : Type v → Type w} [Monad m] (f : USize → β → m β) (s : USizeArray.Slice) (i : Nat) : i ≤ Std.Slice.size s → β → m β

The loop of foldrM: folds f over the first i elements of s, from last to first.

Equations

• ScalarArray.USizeArray.Slice.foldrM.loop f s 0 x_3 a = pure a
• ScalarArray.USizeArray.Slice.foldrM.loop f s i_1.succ h a = do let __do_lift ← f s[i_1] a ScalarArray.USizeArray.Slice.foldrM.loop f s i_1 ⋯ __do_lift

@[inline]

def ScalarArray.USizeArray.Slice.foldrMImpl {β : Type v} {m : Type v → Type w} [Monad m] (f : USize → β → m β) (init : β) (s : USizeArray.Slice) : m β

For internal use only.

Equations

• One or more equations did not get rendered due to their size.

@[csimp]

theorem ScalarArray.USizeArray.Slice.foldrM_eq_foldrMImpl : @foldrM = @foldrMImpl

@[inline]

def ScalarArray.USizeArray.Slice.foldr {β : Type v} (f : USize → β → β) (init : β) (s : USizeArray.Slice) : β

Folds a function over the elements of s, from last to first.

Equations

• ScalarArray.USizeArray.Slice.foldr f init s = (ScalarArray.USizeArray.Slice.foldrM (fun (x1 : USize) (x2 : β) => pure (f x1 x2)) init s).run

@[inline]

def ScalarArray.USizeArray.Slice.forRevM {m : Type v → Type w} [Monad m] (f : USize → m PUnit) (s : USizeArray.Slice) : m PUnit

Runs a monadic action on each element of s, from last to first.

Equations

• ScalarArray.USizeArray.Slice.forRevM f s = ScalarArray.USizeArray.Slice.foldrM (fun (x : USize) (x_1 : PUnit) => f x) PUnit.unit s

def ScalarArray.USizeArray.Slice.findSomeRevM? {β : Type v} {m : Type v → Type w} [Monad m] (s : USizeArray.Slice) (f : USize → m (Option β)) : m (Option β)

The result of the last element of s for which f returns some, searching from the end.

Equations

• s.findSomeRevM? f = ScalarArray.USizeArray.Slice.findSomeRevM?.loop s f (Std.Slice.size s) ⋯

@[specialize #[]]

def ScalarArray.USizeArray.Slice.findSomeRevM?.loop {β : Type v} {m : Type v → Type w} [Monad m] (s : USizeArray.Slice) (f : USize → m (Option β)) (i : Nat) : i ≤ Std.Slice.size s → m (Option β)

The loop of findSomeRevM?: searches the first i elements of s, from the end.

Equations

• One or more equations did not get rendered due to their size.
• ScalarArray.USizeArray.Slice.findSomeRevM?.loop s f 0 x_2 = pure none

@[inline]

def ScalarArray.USizeArray.Slice.findSomeRevMImpl {β : Type v} {m : Type v → Type w} [Monad m] (s : USizeArray.Slice) (f : USize → m (Option β)) : m (Option β)

For internal use only.

Equations

• One or more equations did not get rendered due to their size.

@[csimp]

theorem ScalarArray.USizeArray.Slice.findSomeRevM?_eq_findSomeRevMImpl : @findSomeRevM? = @findSomeRevMImpl

@[inline]

def ScalarArray.USizeArray.Slice.findRevM? {m : Type → Type w} [Monad m] (s : USizeArray.Slice) (p : USize → m Bool) : m (Option USize)

The last element of s that satisfies the monadic predicate p.

Equations

• s.findRevM? p = s.findSomeRevM? fun (x : USize) => do let __do_lift ← p x pure (if __do_lift = true then some x else none)

@[inline]

def ScalarArray.USizeArray.Slice.findRev? (s : USizeArray.Slice) (p : USize → Bool) : Option USize

The last element of s that satisfies p.

Equations

• s.findRev? p = (s.findRevM? fun (x : USize) => pure (p x)).run

@[inline]

def ScalarArray.USizeArray.Slice.find? (s : USizeArray.Slice) (p : USize → Bool) : Option USize

The first element of s that satisfies p.

Equations

• s.find? p = (Std.Slice.iter s).find? p

@[inline]

def ScalarArray.USizeArray.Slice.any (s : USizeArray.Slice) (p : USize → Bool) : Bool

Whether some element of s satisfies p.

Equations

• s.any p = Std.Iter.any p (Std.Slice.iter s)

@[inline]

def ScalarArray.USizeArray.Slice.all (s : USizeArray.Slice) (p : USize → Bool) : Bool

Whether every element of s satisfies p.

Equations

• s.all p = Std.Iter.all p (Std.Slice.iter s)

@[inline]

def ScalarArray.USizeArray.Slice.contains (s : USizeArray.Slice) (v : USize) : Bool

Whether some element of s is == to v.

Equations

• s.contains v = s.any fun (x : USize) => v == x

@[inline]

def ScalarArray.USizeArray.Slice.count (s : USizeArray.Slice) (p : USize → Bool) : Nat

The number of elements of s that satisfy p.

Equations

• s.count p = Std.Iter.fold (fun (n : Nat) (x : USize) => if p x = true then n + 1 else n) 0 (Std.Slice.iter s)

Membership and equality

@[instance_reducible]

instance ScalarArray.USizeArray.Slice.instMembershipUSize : Membership USize USizeArray.Slice

x ∈ s when x is an element of s.

Equations

• ScalarArray.USizeArray.Slice.instMembershipUSize = { mem := fun (s : ScalarArray.USizeArray.Slice) (x : USize) => x ∈ s.copy }

def ScalarArray.USizeArray.Slice.beq (s t : USizeArray.Slice) : Bool

Compares the elements of two slices with ==: slices of different arrays, or at different offsets, are equal when their elements are. Logically it compares the copies.

Equations

• s.beq t = (s.copy == t.copy)

def ScalarArray.USizeArray.Slice.beqImpl (s t : USizeArray.Slice) : Bool

For internal use only.

Equations

• One or more equations did not get rendered due to their size.

@[csimp]

theorem ScalarArray.USizeArray.Slice.beq_eq_beqImpl : beq = beqImpl

@[instance_reducible]

instance ScalarArray.USizeArray.Slice.instBEq : BEq USizeArray.Slice

Equations

• ScalarArray.USizeArray.Slice.instBEq = { beq := ScalarArray.USizeArray.Slice.beq }

Collecting iterators into arrays

@[inline]

def Std.Iter.toUSizeArray {α : Type} [Iterator α Id USize] [IteratorLoop α Id Id] (it : Iter USize) : ScalarArray.USizeArray

Collects the values emitted by an iterator into a new array. Together with the Std.Iterators combinators, this gives functions such as map, filter, take and zipWith, for example (a.iter.map (· + 1)).toUSizeArray.

Equations

• it.toUSizeArray = Std.Iter.fold (fun (x1 : ScalarArray.USizeArray) (x2 : USize) => x1.push x2) ScalarArray.USizeArray.empty it

@[inline]

def Std.Iter.toUSizeArrayWithCapacity {α : Type} [Iterator α Id USize] [IteratorLoop α Id Id] (it : Iter USize) (capacity : Nat) : ScalarArray.USizeArray

Like Std.Iter.toUSizeArray, but the new array starts with room for capacity elements.

Equations

• it.toUSizeArrayWithCapacity capacity = Std.Iter.fold (fun (x1 : ScalarArray.USizeArray) (x2 : USize) => x1.push x2) (ScalarArray.USizeArray.emptyWithCapacity capacity) it

@[simp]

theorem Std.Iter.toUSizeArrayWithCapacity_eq {α : Type} [Iterator α Id USize] [IteratorLoop α Id Id] (it : Iter USize) (capacity : Nat) : it.toUSizeArrayWithCapacity capacity = it.toUSizeArray