Slices of UInt64Array

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

The slice type

structure ScalarArray.UInt64Array.SliceData : Type

Internal representation of UInt64Array.Slice.

• array : UInt64Array

  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.UInt64Array.Slice : Type

A region of a UInt64Array: 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.UInt64Array.Slice = Std.Slice ScalarArray.UInt64Array.SliceData

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

@[inline]

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

The underlying array.

Equations

• s.array = s.internalRepresentation.array

@[inline]

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

The starting index of the slice (inclusive).

Equations

• s.start = s.internalRepresentation.start

@[inline]

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

The ending index of the slice (exclusive).

Equations

• s.stop = s.internalRepresentation.stop

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

The starting index is no later than the ending index.

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

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

@[instance_reducible]

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

Equations

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

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

Reads

@[inline]

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

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.UInt64Array.Slice.instGetElemNatUInt64LtSizeSliceData : GetElem UInt64Array.Slice Nat UInt64 fun (s : UInt64Array.Slice) (i : Nat) => i < Std.Slice.size s

Equations

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

@[inline]

def ScalarArray.UInt64Array.Slice.getD (s : UInt64Array.Slice) (i : Nat) (v₀ : UInt64) : UInt64

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.UInt64Array.Slice.get! (s : UInt64Array.Slice) (i : Nat) : UInt64

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.UInt64Array.Slice.popFront (s : UInt64Array.Slice) : UInt64Array.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.UInt64Array.Slice.empty : UInt64Array.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.UInt64Array.Slice.instEmptyCollection : EmptyCollection UInt64Array.Slice

Equations

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

@[instance_reducible]

instance ScalarArray.UInt64Array.Slice.instInhabited : Inhabited UInt64Array.Slice

Equations

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

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

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.UInt64Array.Slice.getElem_eq (s : UInt64Array.Slice) (i : Nat) (h : i < Std.Slice.size s) : s[i] = s.array[s.start + i]

@[instance_reducible]

instance ScalarArray.UInt64Array.Slice.instRepr : Repr UInt64Array.Slice

Prints the array and the bounds in slice notation, (ScalarArray.UInt64Array.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.UInt64Array.Slice.instToString : ToString UInt64Array.Slice

Equations

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

Slice notation

@[inline]

def ScalarArray.UInt64Array.toSlice (a : UInt64Array) (start : Nat := 0) (stop : Nat := a.size) : UInt64Array.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.UInt64Array.instCoeSlice : Coe UInt64Array UInt64Array.Slice

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[inline]

def ScalarArray.UInt64Array.Slice.slice (s : UInt64Array.Slice) (start : Nat := 0) (stop : Nat := Std.Slice.size s) : UInt64Array.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.UInt64Array.instSliceableSliceNat : Std.Rcc.Sliceable UInt64Array.Slice Nat UInt64Array.Slice

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

Iterators

structure ScalarArray.UInt64Array.SliceIterator : Type

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

• xs : UInt64Array.Slice

  The rest of the slice.

@[inline]

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

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.UInt64Array.instIteratorSliceIteratorIdUInt64 : Std.Iterator UInt64Array.SliceIterator Id UInt64

Equations

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

instance ScalarArray.UInt64Array.instFiniteSliceIteratorIdUInt64 : Std.Iterators.Finite UInt64Array.SliceIterator Id

@[implemented_by _private.ScalarArray.UInt64.Slice.0.ScalarArray.UInt64Array.SliceIterator.forInImpl]

def ScalarArray.UInt64Array.SliceIterator.forIn {n : Type x → Type x'} [Monad n] (lift : (γ : Type) → (δ : Type x) → (γ → n δ) → Id γ → n δ) (γ : Type x) (Pl : UInt64 → γ → ForInStep γ → Prop) (it : Std.IterM Id UInt64) (init : γ) (f : (b : UInt64) → 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.UInt64Array.SliceIterator.forIn lift γ Pl it init f = Std.IteratorLoop.forIn lift γ Pl it init f

@[instance_reducible]

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

Equations

• ScalarArray.UInt64Array.instIteratorLoopSliceIteratorIdUInt64OfMonad = { forIn := ScalarArray.UInt64Array.SliceIterator.forIn }

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

@[instance_reducible]

instance ScalarArray.UInt64Array.instToIteratorSliceSliceDataIdSliceIteratorUInt64 : Std.ToIterator (Std.Slice UInt64Array.SliceData) Id UInt64Array.SliceIterator UInt64

Equations

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

@[instance_reducible]

instance ScalarArray.UInt64Array.instForInSliceUInt64OfMonad {m : Type u_1 → Type u_2} [Monad m] : ForIn m UInt64Array.Slice UInt64

Equations

• ScalarArray.UInt64Array.instForInSliceUInt64OfMonad = inferInstance

@[instance_reducible]

instance ScalarArray.UInt64Array.instForMSliceUInt64OfMonad {m : Type u_1 → Type u_2} [Monad m] : ForM m UInt64Array.Slice UInt64

Equations

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

@[inline]

def Std.Iter.toUInt64Slice (it : Iter UInt64) : ScalarArray.UInt64Array.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.toUInt64Slice = it.internalState.xs

@[inline]

def ScalarArray.UInt64Array.iter (a : UInt64Array) : Std.Iter UInt64

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.UInt64Array.Slice.foldrM {β : Type v} {m : Type v → Type w} [Monad m] (f : UInt64 → β → m β) (init : β) (s : UInt64Array.Slice) : m β

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

Equations

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

@[specialize #[]]

def ScalarArray.UInt64Array.Slice.foldrM.loop {β : Type v} {m : Type v → Type w} [Monad m] (f : UInt64 → β → m β) (s : UInt64Array.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.UInt64Array.Slice.foldrM.loop f s 0 x_3 a = pure a
• ScalarArray.UInt64Array.Slice.foldrM.loop f s i_1.succ h a = do let __do_lift ← f s[i_1] a ScalarArray.UInt64Array.Slice.foldrM.loop f s i_1 ⋯ __do_lift

@[inline]

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

For internal use only.

Equations

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

@[csimp]

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

@[inline]

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

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

Equations

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

@[inline]

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

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

Equations

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

def ScalarArray.UInt64Array.Slice.findSomeRevM? {β : Type v} {m : Type v → Type w} [Monad m] (s : UInt64Array.Slice) (f : UInt64 → 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.UInt64Array.Slice.findSomeRevM?.loop s f (Std.Slice.size s) ⋯

@[specialize #[]]

def ScalarArray.UInt64Array.Slice.findSomeRevM?.loop {β : Type v} {m : Type v → Type w} [Monad m] (s : UInt64Array.Slice) (f : UInt64 → 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.UInt64Array.Slice.findSomeRevM?.loop s f 0 x_2 = pure none

@[inline]

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

For internal use only.

Equations

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

@[csimp]

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

@[inline]

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

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

Equations

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

@[inline]

def ScalarArray.UInt64Array.Slice.findRev? (s : UInt64Array.Slice) (p : UInt64 → Bool) : Option UInt64

The last element of s that satisfies p.

Equations

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

@[inline]

def ScalarArray.UInt64Array.Slice.find? (s : UInt64Array.Slice) (p : UInt64 → Bool) : Option UInt64

The first element of s that satisfies p.

Equations

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

@[inline]

def ScalarArray.UInt64Array.Slice.any (s : UInt64Array.Slice) (p : UInt64 → Bool) : Bool

Whether some element of s satisfies p.

Equations

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

@[inline]

def ScalarArray.UInt64Array.Slice.all (s : UInt64Array.Slice) (p : UInt64 → Bool) : Bool

Whether every element of s satisfies p.

Equations

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

@[inline]

def ScalarArray.UInt64Array.Slice.contains (s : UInt64Array.Slice) (v : UInt64) : Bool

Whether some element of s is == to v.

Equations

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

@[inline]

def ScalarArray.UInt64Array.Slice.count (s : UInt64Array.Slice) (p : UInt64 → Bool) : Nat

The number of elements of s that satisfy p.

Equations

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

Membership and equality

@[instance_reducible]

instance ScalarArray.UInt64Array.Slice.instMembershipUInt64 : Membership UInt64 UInt64Array.Slice

x ∈ s when x is an element of s.

Equations

• ScalarArray.UInt64Array.Slice.instMembershipUInt64 = { mem := fun (s : ScalarArray.UInt64Array.Slice) (x : UInt64) => x ∈ s.copy }

def ScalarArray.UInt64Array.Slice.beq (s t : UInt64Array.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.UInt64Array.Slice.beqImpl (s t : UInt64Array.Slice) : Bool

For internal use only.

Equations

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

@[csimp]

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

@[instance_reducible]

instance ScalarArray.UInt64Array.Slice.instBEq : BEq UInt64Array.Slice

Equations

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

Collecting iterators into arrays

@[inline]

def Std.Iter.toUInt64Array {α : Type} [Iterator α Id UInt64] [IteratorLoop α Id Id] (it : Iter UInt64) : ScalarArray.UInt64Array

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)).toUInt64Array.

Equations

• it.toUInt64Array = Std.Iter.fold (fun (x1 : ScalarArray.UInt64Array) (x2 : UInt64) => x1.push x2) ScalarArray.UInt64Array.empty it

@[inline]

def Std.Iter.toUInt64ArrayWithCapacity {α : Type} [Iterator α Id UInt64] [IteratorLoop α Id Id] (it : Iter UInt64) (capacity : Nat) : ScalarArray.UInt64Array

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

Equations

• it.toUInt64ArrayWithCapacity capacity = Std.Iter.fold (fun (x1 : ScalarArray.UInt64Array) (x2 : UInt64) => x1.push x2) (ScalarArray.UInt64Array.emptyWithCapacity capacity) it

@[simp]

theorem Std.Iter.toUInt64ArrayWithCapacity_eq {α : Type} [Iterator α Id UInt64] [IteratorLoop α Id Id] (it : Iter UInt64) (capacity : Nat) : it.toUInt64ArrayWithCapacity capacity = it.toUInt64Array