Arrays of Int16: array operations

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

Removing elements

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

Whether a has no elements.

Equations

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

@[implemented_by _private.ScalarArray.Int16.Array.0.ScalarArray.Int16Array.popImpl]

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

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

Equations

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

@[inline]

def ScalarArray.Int16Array.back? (a : Int16Array) : Option Int16

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

Equations

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

@[inline]

def ScalarArray.Int16Array.back! (a : Int16Array) : Int16

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

Equations

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

@[inline]

def ScalarArray.Int16Array.back (a : Int16Array) (h : 0 < a.size) : Int16

The last element of a, which is not empty.

Equations

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

@[implemented_by _private.ScalarArray.Int16.Array.0.ScalarArray.Int16Array.popWhileImpl]

def ScalarArray.Int16Array.popWhile (p : Int16 → Bool) (a : Int16Array) : Int16Array

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

Equations

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

@[implemented_by _private.ScalarArray.Int16.Array.0.ScalarArray.Int16Array.extractImpl]

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

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.Int16Array.mk (a.toArray.extract start stop)

Linearity

@[never_extract, extern lean_sarray_mark_linear]

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

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.Int16Array.propagateMark (a : Int16Array) (b : Int16Array) : Int16Array

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.Int16Array.findFinIdx? (a : Int16Array) (p : Int16 → 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.Int16Array.findFinIdx?.loop✝ a p start

@[inline]

def ScalarArray.Int16Array.findIdx? (a : Int16Array) (p : Int16 → 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.Int16Array.findIdx?.loop✝ a p start

Building arrays

@[implemented_by _private.ScalarArray.Int16.Array.0.ScalarArray.Int16Array.replicateImpl]

def ScalarArray.Int16Array.replicate (n : Nat) (v : Int16) : Int16Array

An array of n copies of v.

Equations

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

@[implemented_by _private.ScalarArray.Int16.Array.0.ScalarArray.Int16Array.ofFnImpl]

def ScalarArray.Int16Array.ofFn {n : Nat} (f : Fin n → Int16) : Int16Array

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

Equations

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

def ScalarArray.Int16Array.ofList (l : List Int16) : Int16Array

The array with the elements of l.

Equations

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

def ScalarArray.Int16Array.ofListImpl (l : List Int16) : Int16Array

For internal use only.

Equations

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

@[csimp]

theorem ScalarArray.Int16Array.ofList_eq_ofListImpl : ofList = ofListImpl

Iteration

def ScalarArray.Int16Array.foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → Int16 → m β) (init : β) (a : Int16Array) (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.Int16Array.foldlM f init a start stop = Array.foldlM f init a.toArray start stop

@[inline]

def ScalarArray.Int16Array.foldlMImpl {β : Type v} {m : Type v → Type w} [Monad m] (f : β → Int16 → m β) (init : β) (a : Int16Array) (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.Int16Array.foldlM_eq_foldlMImpl : @foldlM = @foldlMImpl

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

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

Equations

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

@[inline]

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

For internal use only.

Equations

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

@[csimp]

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

@[inline]

def ScalarArray.Int16Array.foldl {β : Type v} (f : β → Int16 → β) (init : β) (a : Int16Array) (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.Int16Array.foldl f init a start stop = (ScalarArray.Int16Array.foldlM (fun (x1 : β) (x2 : Int16) => pure (f x1 x2)) init a start stop).run

@[inline]

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

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

Equations

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

@[inline]

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

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

Equations

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

def ScalarArray.Int16Array.forIn {β : Type v} {m : Type v → Type w} [Monad m] (a : Int16Array) (init : β) (f : Int16 → β → 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.Int16Array.forInImpl {β : Type v} {m : Type v → Type w} [Monad m] (a : Int16Array) (init : β) (f : Int16 → β → m (ForInStep β)) : m β

For internal use only.

Equations

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

@[csimp]

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

@[instance_reducible]

instance ScalarArray.Int16Array.instForInInt16OfMonad {m : Type u_1 → Type u_2} [Monad m] : ForIn m Int16Array Int16

Equations

• ScalarArray.Int16Array.instForInInt16OfMonad = { forIn := fun {β : Type ?u.2} (a : ScalarArray.Int16Array) (b : β) (f : Int16 → β → m (ForInStep β)) => a.forIn b f }

@[instance_reducible]

instance ScalarArray.Int16Array.instForMInt16OfMonad {m : Type u_1 → Type u_2} [Monad m] : ForM m Int16Array Int16

Equations

• ScalarArray.Int16Array.instForMInt16OfMonad = { forM := fun (a : ScalarArray.Int16Array) (f : Int16 → m PUnit) => ScalarArray.Int16Array.forM f a }

def ScalarArray.Int16Array.any (a : Int16Array) (p : Int16 → Bool) : Bool

Whether some element of a satisfies p.

Equations

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

@[inline]

def ScalarArray.Int16Array.anyImpl (a : Int16Array) (p : Int16 → Bool) : Bool

For internal use only.

Equations

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

@[csimp]

theorem ScalarArray.Int16Array.any_eq_anyImpl : any = anyImpl

def ScalarArray.Int16Array.all (a : Int16Array) (p : Int16 → Bool) : Bool

Whether every element of a satisfies p.

Equations

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

@[inline]

def ScalarArray.Int16Array.allImpl (a : Int16Array) (p : Int16 → Bool) : Bool

For internal use only.

Equations

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

@[csimp]

theorem ScalarArray.Int16Array.all_eq_allImpl : all = allImpl

def ScalarArray.Int16Array.contains (a : Int16Array) (v : Int16) : Bool

Whether some element of a is == to v.

Equations

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

def ScalarArray.Int16Array.containsImpl (a : Int16Array) (v : Int16) : Bool

For internal use only.

Equations

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

@[csimp]

theorem ScalarArray.Int16Array.contains_eq_containsImpl : contains = containsImpl

@[instance_reducible]

instance ScalarArray.Int16Array.instMembershipInt16 : Membership Int16 Int16Array

x ∈ a when x is an element of a.

Equations

• ScalarArray.Int16Array.instMembershipInt16 = { mem := fun (a : ScalarArray.Int16Array) (x : Int16) => x ∈ a.toArray }

Equality and hashing

@[extern lean_sarray_dec_eq]

def ScalarArray.Int16Array.decEq (a b : Int16Array) : 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.Int16Array.instDecidableEq : DecidableEq Int16Array

Equations

• ScalarArray.Int16Array.instDecidableEq = ScalarArray.Int16Array.decEq

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

The same hash as a.toArray.

Equations

• a.hash = hash a.toArray

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

For internal use only.

Equations

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

@[csimp]

theorem ScalarArray.Int16Array.hash_eq_hashImpl : hash = hashImpl

@[instance_reducible]

instance ScalarArray.Int16Array.instHashable : Hashable Int16Array

Equations

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

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

Conversion and printing

def ScalarArray.Int16Array.toList (a : Int16Array) : List Int16

The elements of a as a list.

Equations

• a.toList = a.toArray.toList

@[instance_reducible]

instance ScalarArray.Int16Array.instRepr : Repr Int16Array

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

Equations

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

@[instance_reducible]

instance ScalarArray.Int16Array.instToString : ToString Int16Array

Equations

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

@[inline]

def List.toInt16Array (l : List Int16) : ScalarArray.Int16Array

The array with the elements of l.

Equations

• l.toInt16Array = ScalarArray.Int16Array.ofList l