Arrays of UInt64: array operations

Removing elements, search, building arrays, iteration, equality, hashing and printing.

Removing elements

def ScalarArray.UInt64Array.isEmpty (a : UInt64Array) : Bool

Whether a has no elements.

Equations

• a.isEmpty = (a.size == 0)

@[implemented_by _private.ScalarArray.UInt64.Array.0.ScalarArray.UInt64Array.popImpl]

def ScalarArray.UInt64Array.pop (a : UInt64Array) : UInt64Array

Removes the last element of a, if any, in place when a is not shared.

Equations

• a.pop = ScalarArray.UInt64Array.mk a.toArray.pop

@[inline]

def ScalarArray.UInt64Array.back? (a : UInt64Array) : Option UInt64

The last element of a, or none if a is empty.

Equations

• a.back? = a[a.size - 1]?

@[inline]

def ScalarArray.UInt64Array.back! (a : UInt64Array) : UInt64

The last element of a. Panics if a is empty, and then returns default.

Equations

• a.back! = a[a.size - 1]!

@[inline]

def ScalarArray.UInt64Array.back (a : UInt64Array) (h : 0 < a.size) : UInt64

The last element of a, which is not empty.

Equations

• a.back h = a[a.size - 1]

@[implemented_by _private.ScalarArray.UInt64.Array.0.ScalarArray.UInt64Array.popWhileImpl]

def ScalarArray.UInt64Array.popWhile (p : UInt64 → Bool) (a : UInt64Array) : UInt64Array

Removes the longest run of elements at the end of a that satisfy p, in place when a is not shared.

Equations

• ScalarArray.UInt64Array.popWhile p a = ScalarArray.UInt64Array.mk (Array.popWhile p a.toArray)

@[implemented_by _private.ScalarArray.UInt64.Array.0.ScalarArray.UInt64Array.extractImpl]

def ScalarArray.UInt64Array.extract (a : UInt64Array) (start stop : Nat) : UInt64Array

The elements of a from index start up to, but not including, min stop a.size, copied into a new array.

Equations

• a.extract start stop = ScalarArray.UInt64Array.mk (a.toArray.extract start stop)

Linearity

@[never_extract, extern lean_sarray_mark_linear]

def ScalarArray.UInt64Array.markLinear (a : UInt64Array) : UInt64Array

Marks a as linear, a debugging aid: if a marked array is ever copied because it is shared when it needs to be exclusive, as before an in-place write, the runtime panics. The mark goes on an exclusive array, so if a is shared it is copied first and the copy is marked. Logically this is the identity.

Equations

• a.markLinear = a

@[never_extract, extern lean_sarray_propagate_mark]

def ScalarArray.UInt64Array.propagateMark (a : UInt64Array) (b : UInt64Array) : UInt64Array

Returns b, marked as linear if a is marked. Like markLinear, marking copies b first if it is shared. Logically this is b.

Equations

• a.propagateMark b = b

Search

@[inline]

def ScalarArray.UInt64Array.findFinIdx? (a : UInt64Array) (p : UInt64 → Bool) (start : Nat := 0) : Option (Fin a.size)

The index of the first element at or after start that satisfies p, with a proof that it is in bounds.

Equations

• a.findFinIdx? p start = ScalarArray.UInt64Array.findFinIdx?.loop✝ a p start

@[inline]

def ScalarArray.UInt64Array.findIdx? (a : UInt64Array) (p : UInt64 → Bool) (start : Nat := 0) : Option Nat

The index of the first element at or after start that satisfies p.

Equations

• a.findIdx? p start = ScalarArray.UInt64Array.findIdx?.loop✝ a p start

Building arrays

@[implemented_by _private.ScalarArray.UInt64.Array.0.ScalarArray.UInt64Array.replicateImpl]

def ScalarArray.UInt64Array.replicate (n : Nat) (v : UInt64) : UInt64Array

An array of n copies of v.

Equations

• ScalarArray.UInt64Array.replicate n v = ScalarArray.UInt64Array.mk (Array.replicate n v)

@[implemented_by _private.ScalarArray.UInt64.Array.0.ScalarArray.UInt64Array.ofFnImpl]

def ScalarArray.UInt64Array.ofFn {n : Nat} (f : Fin n → UInt64) : UInt64Array

The array #[f 0, …, f (n - 1)].

Equations

• ScalarArray.UInt64Array.ofFn f = ScalarArray.UInt64Array.mk (Array.ofFn f)

def ScalarArray.UInt64Array.ofList (l : List UInt64) : UInt64Array

The array with the elements of l.

Equations

• ScalarArray.UInt64Array.ofList l = ScalarArray.UInt64Array.mk l.toArray

def ScalarArray.UInt64Array.ofListImpl (l : List UInt64) : UInt64Array

For internal use only.

Equations

• ScalarArray.UInt64Array.ofListImpl l = ScalarArray.UInt64Array.ofListImpl.loop✝ l (ScalarArray.UInt64Array.emptyWithCapacity l.length)

@[csimp]

theorem ScalarArray.UInt64Array.ofList_eq_ofListImpl : ofList = ofListImpl

Iteration

def ScalarArray.UInt64Array.foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt64 → m β) (init : β) (a : UInt64Array) (start : Nat := 0) (stop : Nat := a.size) : m β

Folds a monadic function over the elements of a from index start up to, but not including, stop, from first to last.

Equations

• ScalarArray.UInt64Array.foldlM f init a start stop = Array.foldlM f init a.toArray start stop

@[inline]

def ScalarArray.UInt64Array.foldlMImpl {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt64 → m β) (init : β) (a : UInt64Array) (start : Nat := 0) (stop : Nat := a.size) : m β

For internal use only.

Equations

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

@[csimp]

theorem ScalarArray.UInt64Array.foldlM_eq_foldlMImpl : @foldlM = @foldlMImpl

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

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

Equations

• ScalarArray.UInt64Array.foldrM f init a = Array.foldrM f init a.toArray

@[inline]

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

For internal use only.

Equations

• ScalarArray.UInt64Array.foldrMImpl f init a = if a.size < USize.size then ScalarArray.UInt64Array.foldrMImpl.loop✝ f a a.usize ⋯ init else ScalarArray.UInt64Array.foldrMSlow✝ f init a

@[csimp]

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

@[inline]

def ScalarArray.UInt64Array.foldl {β : Type v} (f : β → UInt64 → β) (init : β) (a : UInt64Array) (start : Nat := 0) (stop : Nat := a.size) : β

Folds a function over the elements of a from index start up to, but not including, stop, from first to last.

Equations

• ScalarArray.UInt64Array.foldl f init a start stop = (ScalarArray.UInt64Array.foldlM (fun (x1 : β) (x2 : UInt64) => pure (f x1 x2)) init a start stop).run

@[inline]

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

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

Equations

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

@[inline]

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

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

Equations

• ScalarArray.UInt64Array.forM f a = ScalarArray.UInt64Array.foldlM (fun (x : PUnit) (x_1 : UInt64) => f x_1) PUnit.unit a

def ScalarArray.UInt64Array.forIn {β : Type v} {m : Type v → Type w} [Monad m] (a : UInt64Array) (init : β) (f : UInt64 → β → m (ForInStep β)) : m β

The loop behind for x in a. Logically it is the loop over a.toArray.

Equations

• a.forIn init f = forIn a.toArray init f

@[inline]

def ScalarArray.UInt64Array.forInImpl {β : Type v} {m : Type v → Type w} [Monad m] (a : UInt64Array) (init : β) (f : UInt64 → β → m (ForInStep β)) : m β

For internal use only.

Equations

• a.forInImpl init f = if a.size < USize.size then ScalarArray.UInt64Array.forInImpl.loop✝ a f a.usize ⋯ 0 init else ScalarArray.UInt64Array.forInSlow✝ a init f

@[csimp]

theorem ScalarArray.UInt64Array.forIn_eq_forInImpl : @forIn = @forInImpl

@[instance_reducible]

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

Equations

• ScalarArray.UInt64Array.instForInUInt64OfMonad = { forIn := fun {β : Type ?u.2} (a : ScalarArray.UInt64Array) (b : β) (f : UInt64 → β → m (ForInStep β)) => a.forIn b f }

@[instance_reducible]

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

Equations

• ScalarArray.UInt64Array.instForMUInt64OfMonad = { forM := fun (a : ScalarArray.UInt64Array) (f : UInt64 → m PUnit) => ScalarArray.UInt64Array.forM f a }

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

Whether some element of a satisfies p.

Equations

• a.any p = a.toArray.any p

@[inline]

def ScalarArray.UInt64Array.anyImpl (a : UInt64Array) (p : UInt64 → Bool) : Bool

For internal use only.

Equations

• a.anyImpl p = if a.size < USize.size then ScalarArray.UInt64Array.anyImpl.loop✝ a p a.usize ⋯ 0 else ScalarArray.UInt64Array.anySlow✝ a p

@[csimp]

theorem ScalarArray.UInt64Array.any_eq_anyImpl : any = anyImpl

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

Whether every element of a satisfies p.

Equations

• a.all p = a.toArray.all p

@[inline]

def ScalarArray.UInt64Array.allImpl (a : UInt64Array) (p : UInt64 → Bool) : Bool

For internal use only.

Equations

• a.allImpl p = if a.size < USize.size then ScalarArray.UInt64Array.allImpl.loop✝ a p a.usize ⋯ 0 else ScalarArray.UInt64Array.allSlow✝ a p

@[csimp]

theorem ScalarArray.UInt64Array.all_eq_allImpl : all = allImpl

def ScalarArray.UInt64Array.contains (a : UInt64Array) (v : UInt64) : Bool

Whether some element of a is == to v.

Equations

• a.contains v = a.toArray.contains v

def ScalarArray.UInt64Array.containsImpl (a : UInt64Array) (v : UInt64) : Bool

For internal use only.

Equations

• a.containsImpl v = a.any fun (x : UInt64) => v == x

@[csimp]

theorem ScalarArray.UInt64Array.contains_eq_containsImpl : contains = containsImpl

@[instance_reducible]

instance ScalarArray.UInt64Array.instMembershipUInt64 : Membership UInt64 UInt64Array

x ∈ a when x is an element of a.

Equations

• ScalarArray.UInt64Array.instMembershipUInt64 = { mem := fun (a : ScalarArray.UInt64Array) (x : UInt64) => x ∈ a.toArray }

Equality and hashing

@[extern lean_sarray_dec_eq]

def ScalarArray.UInt64Array.decEq (a b : UInt64Array) : Decidable (a = b)

Decides equality by comparing the two arrays' memory.

Equations

• a.decEq b = decidable_of_iff (a.toArray = b.toArray) ⋯

@[instance_reducible]

instance ScalarArray.UInt64Array.instDecidableEq : DecidableEq UInt64Array

Equations

• ScalarArray.UInt64Array.instDecidableEq = ScalarArray.UInt64Array.decEq

def ScalarArray.UInt64Array.hash (a : UInt64Array) : UInt64

The same hash as a.toArray.

Equations

• a.hash = hash a.toArray

def ScalarArray.UInt64Array.hashImpl (a : UInt64Array) : UInt64

For internal use only.

Equations

• a.hashImpl = ScalarArray.UInt64Array.foldl (fun (r x : UInt64) => mixHash r (hash x)) 7 a

@[csimp]

theorem ScalarArray.UInt64Array.hash_eq_hashImpl : hash = hashImpl

@[instance_reducible]

instance ScalarArray.UInt64Array.instHashable : Hashable UInt64Array

Equations

• ScalarArray.UInt64Array.instHashable = { hash := ScalarArray.UInt64Array.hash }

theorem ScalarArray.UInt64Array.hash_eq_hash_toArray (a : UInt64Array) : Hashable.hash a = Hashable.hash a.toArray

Conversion and printing

def ScalarArray.UInt64Array.toList (a : UInt64Array) : List UInt64

The elements of a as a list.

Equations

• a.toList = a.toArray.toList

@[instance_reducible]

instance ScalarArray.UInt64Array.instRepr : Repr UInt64Array

Prints ScalarArray.UInt64Array.mk #[...], which evaluates to an equal array.

Equations

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

@[instance_reducible]

instance ScalarArray.UInt64Array.instToString : ToString UInt64Array

Equations

• ScalarArray.UInt64Array.instToString = { toString := fun (a : ScalarArray.UInt64Array) => "UInt64Array.mk " ++ toString a.toArray }

@[inline]

def List.toUInt64Array (l : List UInt64) : ScalarArray.UInt64Array

The array with the elements of l.

Equations

• l.toUInt64Array = ScalarArray.UInt64Array.ofList l