Arrays of Int8: array operations

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

Removing elements

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

Whether a has no elements.

Equations

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

@[implemented_by _private.ScalarArray.Int8.Array.0.ScalarArray.Int8Array.popImpl]

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

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

Equations

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

@[inline]

def ScalarArray.Int8Array.back? (a : Int8Array) : Option Int8

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

Equations

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

@[inline]

def ScalarArray.Int8Array.back! (a : Int8Array) : Int8

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

Equations

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

@[inline]

def ScalarArray.Int8Array.back (a : Int8Array) (h : 0 < a.size) : Int8

The last element of a, which is not empty.

Equations

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

@[implemented_by _private.ScalarArray.Int8.Array.0.ScalarArray.Int8Array.popWhileImpl]

def ScalarArray.Int8Array.popWhile (p : Int8 → Bool) (a : Int8Array) : Int8Array

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

Equations

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

@[implemented_by _private.ScalarArray.Int8.Array.0.ScalarArray.Int8Array.extractImpl]

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

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

Linearity

@[never_extract, extern lean_sarray_mark_linear]

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

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

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

@[inline]

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

Building arrays

@[implemented_by _private.ScalarArray.Int8.Array.0.ScalarArray.Int8Array.replicateImpl]

def ScalarArray.Int8Array.replicate (n : Nat) (v : Int8) : Int8Array

An array of n copies of v.

Equations

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

@[implemented_by _private.ScalarArray.Int8.Array.0.ScalarArray.Int8Array.ofFnImpl]

def ScalarArray.Int8Array.ofFn {n : Nat} (f : Fin n → Int8) : Int8Array

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

Equations

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

def ScalarArray.Int8Array.ofList (l : List Int8) : Int8Array

The array with the elements of l.

Equations

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

def ScalarArray.Int8Array.ofListImpl (l : List Int8) : Int8Array

For internal use only.

Equations

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

@[csimp]

theorem ScalarArray.Int8Array.ofList_eq_ofListImpl : ofList = ofListImpl

Iteration

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

@[inline]

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

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

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

Equations

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

@[inline]

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

For internal use only.

Equations

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

@[csimp]

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

@[inline]

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

@[inline]

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

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

Equations

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

@[inline]

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

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

Equations

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

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

For internal use only.

Equations

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

@[csimp]

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

@[instance_reducible]

instance ScalarArray.Int8Array.instForInInt8OfMonad {m : Type u_1 → Type u_2} [Monad m] : ForIn m Int8Array Int8

Equations

• ScalarArray.Int8Array.instForInInt8OfMonad = { forIn := fun {β : Type ?u.2} (a : ScalarArray.Int8Array) (b : β) (f : Int8 → β → m (ForInStep β)) => a.forIn b f }

@[instance_reducible]

instance ScalarArray.Int8Array.instForMInt8OfMonad {m : Type u_1 → Type u_2} [Monad m] : ForM m Int8Array Int8

Equations

• ScalarArray.Int8Array.instForMInt8OfMonad = { forM := fun (a : ScalarArray.Int8Array) (f : Int8 → m PUnit) => ScalarArray.Int8Array.forM f a }

def ScalarArray.Int8Array.any (a : Int8Array) (p : Int8 → Bool) : Bool

Whether some element of a satisfies p.

Equations

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

@[inline]

def ScalarArray.Int8Array.anyImpl (a : Int8Array) (p : Int8 → Bool) : Bool

For internal use only.

Equations

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

@[csimp]

theorem ScalarArray.Int8Array.any_eq_anyImpl : any = anyImpl

def ScalarArray.Int8Array.all (a : Int8Array) (p : Int8 → Bool) : Bool

Whether every element of a satisfies p.

Equations

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

@[inline]

def ScalarArray.Int8Array.allImpl (a : Int8Array) (p : Int8 → Bool) : Bool

For internal use only.

Equations

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

@[csimp]

theorem ScalarArray.Int8Array.all_eq_allImpl : all = allImpl

def ScalarArray.Int8Array.contains (a : Int8Array) (v : Int8) : Bool

Whether some element of a is == to v.

Equations

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

def ScalarArray.Int8Array.containsImpl (a : Int8Array) (v : Int8) : Bool

For internal use only.

Equations

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

@[csimp]

theorem ScalarArray.Int8Array.contains_eq_containsImpl : contains = containsImpl

@[instance_reducible]

instance ScalarArray.Int8Array.instMembershipInt8 : Membership Int8 Int8Array

x ∈ a when x is an element of a.

Equations

• ScalarArray.Int8Array.instMembershipInt8 = { mem := fun (a : ScalarArray.Int8Array) (x : Int8) => x ∈ a.toArray }

Equality and hashing

@[extern lean_sarray_dec_eq]

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

Equations

• ScalarArray.Int8Array.instDecidableEq = ScalarArray.Int8Array.decEq

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

The same hash as a.toArray.

Equations

• a.hash = hash a.toArray

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

For internal use only.

Equations

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

@[csimp]

theorem ScalarArray.Int8Array.hash_eq_hashImpl : hash = hashImpl

@[instance_reducible]

instance ScalarArray.Int8Array.instHashable : Hashable Int8Array

Equations

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

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

Conversion and printing

def ScalarArray.Int8Array.toList (a : Int8Array) : List Int8

The elements of a as a list.

Equations

• a.toList = a.toArray.toList

@[instance_reducible]

instance ScalarArray.Int8Array.instRepr : Repr Int8Array

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

Equations

• ScalarArray.Int8Array.instRepr = { reprPrec := fun (a : ScalarArray.Int8Array) (prec : Nat) => Repr.addAppParen (Std.Format.text "ScalarArray.Int8Array.mk " ++ reprArg a.toArray) prec }

@[instance_reducible]

instance ScalarArray.Int8Array.instToString : ToString Int8Array

Equations

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

@[inline]

def List.toInt8Array (l : List Int8) : ScalarArray.Int8Array

The array with the elements of l.

Equations

• l.toInt8Array = ScalarArray.Int8Array.ofList l