Documentation

ScalarArray.UInt16.Lemmas

Lemmas about UInt16Array #

Lemmas about arrays and slices, stated in terms of the model Array UInt16 and List UInt16.

Arrays #

source
@[simp]
theorem ScalarArray.UInt16Array.size_mk (a : Array UInt16) :
(mk a).size = a.size
source
theorem ScalarArray.UInt16Array.size_eq_toArray_size (a : UInt16Array) :
a.size = a.toArray.size
source
@[simp]
theorem ScalarArray.UInt16Array.size_toArray (a : UInt16Array) :
a.toArray.size = a.size
source
@[simp]
theorem ScalarArray.UInt16Array.size_uset (a : UInt16Array) (i : USize) (v : UInt16) (h : i.toNat < a.size) :
(a.uset i v h).size = a.size
source
@[simp]
theorem ScalarArray.UInt16Array.size_set (a : UInt16Array) (i : Nat) (v : UInt16) (h : i < a.size) :
(a.set i v h).size = a.size
source
@[simp]
theorem ScalarArray.UInt16Array.size_push (a : UInt16Array) (v : UInt16) :
(a.push v).size = a.size + 1
source
@[simp]
theorem ScalarArray.UInt16Array.toArray_append (a b : UInt16Array) :
(a ++ b).toArray = a.toArray ++ b.toArray
source
@[simp]
theorem ScalarArray.UInt16Array.size_append (a b : UInt16Array) :
(a ++ b).size = a.size + b.size
source
theorem ScalarArray.UInt16Array.ext {a b : UInt16Array} (h : a.toArray = b.toArray) :
a = b
source
theorem ScalarArray.UInt16Array.ext_iff {a b : UInt16Array} :
a = b ↔ a.toArray = b.toArray
source
@[simp]
theorem ScalarArray.UInt16Array.toArray_inj {a b : UInt16Array} :
a.toArray = b.toArray ↔ a = b
source
@[simp]
theorem ScalarArray.UInt16Array.getElem_mk (a : Array UInt16) (i : Nat) (h : i < (mk a).size) :
(mk a)[i] = a[i]
source
theorem ScalarArray.UInt16Array.getElem_eq_getElem_toArray (a : UInt16Array) (i : Nat) (h : i < a.size) :
a[i] = a.toArray[i]
source
@[simp]
theorem ScalarArray.UInt16Array.getElem_toArray (a : UInt16Array) (i : Nat) (h : i < a.toArray.size) :
a.toArray[i] = a[i]
source
theorem ScalarArray.UInt16Array.ext_getElem {a b : UInt16Array} (h₁ : a.size = b.size) (h₂ : ∀ (i : Nat) (hi₁ : i < a.size) (hi₂ : i < b.size), a[i] = b[i]) :
a = b
source
@[simp]
theorem ScalarArray.UInt16Array.getElem_usize (a : UInt16Array) (i : USize) (h : i.toNat < a.size) :
a[i] = a[i.toNat]
source
@[simp]
theorem ScalarArray.UInt16Array.toArray_uset (a : UInt16Array) (i : USize) (v : UInt16) (h : i.toNat < a.size) :
(a.uset i v h).toArray = a.toArray.set i.toNat v ⋯
source
@[simp]
theorem ScalarArray.UInt16Array.toArray_set (a : UInt16Array) (i : Nat) (v : UInt16) (h : i < a.size) :
(a.set i v h).toArray = a.toArray.set i v ⋯
source
@[simp]
theorem ScalarArray.UInt16Array.toArray_push (a : UInt16Array) (v : UInt16) :
(a.push v).toArray = a.toArray.push v
source
@[simp]
theorem ScalarArray.UInt16Array.toArray_pop (a : UInt16Array) :
a.pop.toArray = a.toArray.pop
source
@[simp]
theorem ScalarArray.UInt16Array.toArray_extract (a : UInt16Array) (start stop : Nat) :
(a.extract start stop).toArray = a.toArray.extract start stop
source
@[simp]
theorem ScalarArray.UInt16Array.toArray_replicate (n : Nat) (v : UInt16) :
(replicate n v).toArray = Array.replicate n v
source
@[simp]
theorem ScalarArray.UInt16Array.toArray_ofFn {n : Nat} (f : Fin n → UInt16) :
(ofFn f).toArray = Array.ofFn f
source
@[simp]
theorem ScalarArray.UInt16Array.toArray_empty :
empty.toArray = #[]
source
@[simp]
theorem ScalarArray.UInt16Array.size_pop (a : UInt16Array) :
a.pop.size = a.size - 1
source
@[simp]
theorem ScalarArray.UInt16Array.size_extract (a : UInt16Array) (start stop : Nat) :
(a.extract start stop).size = min stop a.size - start
source
@[simp]
theorem ScalarArray.UInt16Array.size_replicate (n : Nat) (v : UInt16) :
(replicate n v).size = n
source
@[simp]
theorem ScalarArray.UInt16Array.size_ofFn {n : Nat} (f : Fin n → UInt16) :
(ofFn f).size = n
source
@[simp]
theorem ScalarArray.UInt16Array.size_empty :
empty.size = 0
source
@[simp]
theorem ScalarArray.UInt16Array.getElem_set (a : UInt16Array) (i : Nat) (v : UInt16) (h : i < a.size) (j : Nat) (hj : j < (a.set i v h).size) :
(a.set i v h)[j] = if i = j then v else a[j]
source
@[simp]
theorem ScalarArray.UInt16Array.getElem_push (a : UInt16Array) (v : UInt16) (i : Nat) (h : i < (a.push v).size) :
(a.push v)[i] = if h' : i < a.size then a[i] else v
source
@[simp]
theorem ScalarArray.UInt16Array.getElem_pop (a : UInt16Array) (i : Nat) (h : i < a.pop.size) :
a.pop[i] = a[i]
source
@[simp]
theorem ScalarArray.UInt16Array.toArray_popWhile (p : UInt16 → Bool) (a : UInt16Array) :
(popWhile p a).toArray = Array.popWhile p a.toArray
source
@[simp]
theorem ScalarArray.UInt16Array.getElem_append (a b : UInt16Array) (i : Nat) (h : i < (a ++ b).size) :
(a ++ b)[i] = if h' : i < a.size then a[i] else b[i - a.size]
source
@[simp]
theorem ScalarArray.UInt16Array.getElem_extract (a : UInt16Array) (start stop i : Nat) (h : i < (a.extract start stop).size) :
(a.extract start stop)[i] = a[start + i]
source
@[simp]
theorem ScalarArray.UInt16Array.getElem_replicate (n : Nat) (v : UInt16) (i : Nat) (h : i < (replicate n v).size) :
(replicate n v)[i] = v
source
@[simp]
theorem ScalarArray.UInt16Array.getElem_ofFn {n : Nat} (f : Fin n → UInt16) (i : Nat) (h : i < (ofFn f).size) :
(ofFn f)[i] = f ⟨i, ⋯⟩
source
theorem ScalarArray.UInt16Array.foldl_eq_foldl_toArray {β : Type v} (f : β → UInt16 → β) (init : β) (a : UInt16Array) :
foldl f init a = Array.foldl f init a.toArray
source
theorem ScalarArray.UInt16Array.foldr_eq_foldr_toArray {β : Type v} (f : UInt16 → β → β) (init : β) (a : UInt16Array) :
foldr f init a = Array.foldr f init a.toArray
source
@[simp]
theorem ScalarArray.UInt16Array.toList_toArray (a : UInt16Array) :
a.toArray.toList = a.toList
source
@[simp]
theorem ScalarArray.UInt16Array.emptyc_eq_empty :
∅ = empty
source
@[simp]
theorem ScalarArray.UInt16Array.emptyWithCapacity_eq_empty (c : Nat) :
emptyWithCapacity c = empty
source
theorem ScalarArray.UInt16Array.size_eq_zero_iff {a : UInt16Array} :
a.size = 0 ↔ a = empty
source
@[simp]
theorem ScalarArray.UInt16Array.toArray_set! (a : UInt16Array) (i : Nat) (v : UInt16) :
(a.set! i v).toArray = a.toArray.set! i v
source
@[simp]
theorem ScalarArray.UInt16Array.size_set! (a : UInt16Array) (i : Nat) (v : UInt16) :
(a.set! i v).size = a.size
source
theorem ScalarArray.UInt16Array.getElem!_eq_getElem!_toArray (a : UInt16Array) (i : Nat) :
a[i]! = a.toArray[i]!
source
@[simp]
theorem ScalarArray.UInt16Array.toArray_ofList (l : List UInt16) :
(ofList l).toArray = l.toArray
source
@[simp]
theorem ScalarArray.UInt16Array.size_ofList (l : List UInt16) :
(ofList l).size = l.length
source
@[simp]
theorem ScalarArray.UInt16Array.getElem_ofList (l : List UInt16) (i : Nat) (h : i < (ofList l).size) :
(ofList l)[i] = l[i]
source
@[simp]
theorem ScalarArray.UInt16Array.toList_ofList (l : List UInt16) :
(ofList l).toList = l
source
@[simp]
theorem ScalarArray.UInt16Array.ofList_toList (a : UInt16Array) :
ofList a.toList = a
source
@[simp]
theorem ScalarArray.UInt16Array.ensureExclusive_eq (a : UInt16Array) :
a.ensureExclusive = a
source
@[simp]
theorem ScalarArray.UInt16Array.ensureCapacity_eq (a : UInt16Array) (n : Nat) :
a.ensureCapacity n = a
source
@[simp]
theorem ScalarArray.UInt16Array.ensureExclusiveWithCapacity_eq (a : UInt16Array) (n : Nat) :
a.ensureExclusiveWithCapacity n = a
source
@[simp]
theorem ScalarArray.UInt16Array.markLinear_eq (a : UInt16Array) :
a.markLinear = a
source
@[simp]
theorem ScalarArray.UInt16Array.propagateMark_eq (a b : UInt16Array) :
a.propagateMark b = b
source
@[simp]
theorem ScalarArray.UInt16Array.append_empty (a : UInt16Array) :
a ++ empty = a
source
@[simp]
theorem ScalarArray.UInt16Array.empty_append (a : UInt16Array) :
empty ++ a = a
source
theorem ScalarArray.UInt16Array.append_assoc (a b c : UInt16Array) :
a ++ b ++ c = a ++ (b ++ c)
source
@[simp]
theorem ScalarArray.UInt16Array.append_eq_empty_iff {a b : UInt16Array} :
a ++ b = empty ↔ a = empty ∧ b = empty
source
@[simp]
theorem ScalarArray.UInt16Array.append_right_inj (a : UInt16Array) {b c : UInt16Array} :
a ++ b = a ++ c ↔ b = c
source
@[simp]
theorem ScalarArray.UInt16Array.append_left_inj {a b : UInt16Array} (c : UInt16Array) :
a ++ c = b ++ c ↔ a = b
source
theorem ScalarArray.UInt16Array.getElem_append_left {a b : UInt16Array} {i : Nat} (h : i < a.size) :
(a ++ b)[i] = a[i]
source
theorem ScalarArray.UInt16Array.getElem_append_right {a b : UInt16Array} {i : Nat} (h : a.size ≤ i) (h' : i < (a ++ b).size) :
(a ++ b)[i] = b[i - a.size]
source
@[simp]
theorem ScalarArray.UInt16Array.extract_same (a : UInt16Array) (i : Nat) :
a.extract i i = empty
source
@[simp]
theorem ScalarArray.UInt16Array.extract_zero_size (a : UInt16Array) :
a.extract 0 a.size = a
source
@[simp]
theorem ScalarArray.UInt16Array.extract_eq_empty_iff {a : UInt16Array} {i j : Nat} :
a.extract i j = empty ↔ min j a.size ≤ i
source
theorem ScalarArray.UInt16Array.extract_extract (a : UInt16Array) (i j k l : Nat) :
(a.extract i j).extract k l = a.extract (i + k) (min (i + l) j)
source
theorem ScalarArray.UInt16Array.extract_append_extract (a : UInt16Array) (i j k : Nat) :
a.extract i j ++ a.extract j k = a.extract (min i j) (max j k)
source
@[simp]
theorem ScalarArray.UInt16Array.extract_append_eq_left (a b : UInt16Array) :
(a ++ b).extract 0 a.size = a
source
@[simp]
theorem ScalarArray.UInt16Array.extract_append_eq_right (a b : UInt16Array) :
(a ++ b).extract a.size (a.size + b.size) = b
source
@[simp]
theorem ScalarArray.UInt16Array.toArray_copySlice (src : UInt16Array) (srcOff : Nat) (dest : UInt16Array) (destOff len : Nat) (exact : Bool) :
(src.copySlice srcOff dest destOff len exact).toArray = dest.toArray.extract 0 destOff ++ src.toArray.extract srcOff (srcOff + len) ++ dest.toArray.extract (destOff + min len (src.size - srcOff)) dest.size
source
theorem ScalarArray.UInt16Array.copySlice_eq_append (src : UInt16Array) (srcOff : Nat) (dest : UInt16Array) (destOff len : Nat) (exact : Bool) :
src.copySlice srcOff dest destOff len exact = dest.extract 0 destOff ++ src.extract srcOff (srcOff + len) ++ dest.extract (destOff + min len (src.size - srcOff)) dest.size

Lists #

source
@[simp]
theorem ScalarArray.UInt16Array.toList_mk (a : Array UInt16) :
(mk a).toList = a.toList
source
@[simp]
theorem ScalarArray.UInt16Array.length_toList (a : UInt16Array) :
a.toList.length = a.size
source
@[simp]
theorem ScalarArray.UInt16Array.getElem_toList (a : UInt16Array) (i : Nat) (h : i < a.toList.length) :
a.toList[i] = a[i]
source
@[simp]
theorem ScalarArray.UInt16Array.getElem?_toList (a : UInt16Array) (i : Nat) :
a.toList[i]? = a[i]?
source
@[simp]
theorem ScalarArray.UInt16Array.toList_inj {a b : UInt16Array} :
a.toList = b.toList ↔ a = b
source
theorem ScalarArray.UInt16Array.ext_getElem? {a b : UInt16Array} (h : ∀ (i : Nat), a[i]? = b[i]?) :
a = b
source
@[simp]
theorem ScalarArray.UInt16Array.toList_empty :
empty.toList = []
source
@[simp]
theorem ScalarArray.UInt16Array.toList_push (a : UInt16Array) (v : UInt16) :
(a.push v).toList = a.toList ++ [v]
source
@[simp]
theorem ScalarArray.UInt16Array.toList_pop (a : UInt16Array) :
a.pop.toList = a.toList.dropLast
source
@[simp]
theorem ScalarArray.UInt16Array.toList_append (a b : UInt16Array) :
(a ++ b).toList = a.toList ++ b.toList
source
@[simp]
theorem ScalarArray.UInt16Array.toList_set (a : UInt16Array) (i : Nat) (v : UInt16) (h : i < a.size) :
(a.set i v h).toList = a.toList.set i v
source
@[simp]
theorem ScalarArray.UInt16Array.toList_set! (a : UInt16Array) (i : Nat) (v : UInt16) :
(a.set! i v).toList = a.toList.set i v
source
@[simp]
theorem ScalarArray.UInt16Array.toList_extract (a : UInt16Array) (start stop : Nat) :
(a.extract start stop).toList = a.toList.extract start stop
source
@[simp]
theorem ScalarArray.UInt16Array.toList_replicate (n : Nat) (v : UInt16) :
(replicate n v).toList = List.replicate n v
source
@[simp]
theorem ScalarArray.UInt16Array.toList_ofFn {n : Nat} (f : Fin n → UInt16) :
(ofFn f).toList = List.ofFn f
source
@[simp]
theorem ScalarArray.UInt16Array.toList_popWhile (p : UInt16 → Bool) (a : UInt16Array) :
(popWhile p a).toList = (List.dropWhile p a.toList.reverse).reverse
source
@[simp]
theorem ScalarArray.UInt16Array.toList_uset (a : UInt16Array) (i : USize) (v : UInt16) (h : i.toNat < a.size) :
(a.uset i v h).toList = a.toList.set i.toNat v
source
@[simp]
theorem ScalarArray.UInt16Array.toList_copySlice (src : UInt16Array) (srcOff : Nat) (dest : UInt16Array) (destOff len : Nat) (exact : Bool) :
(src.copySlice srcOff dest destOff len exact).toList = dest.toList.extract 0 destOff ++ src.toList.extract srcOff (srcOff + len) ++ dest.toList.extract (destOff + min len (src.size - srcOff)) dest.size

Accessors #

source
@[simp]
theorem ScalarArray.UInt16Array.get_eq_getElem (a : UInt16Array) (i : Nat) (h : i < a.size) :
a.get i h = a[i]
source
@[simp]
theorem ScalarArray.UInt16Array.uget_eq_getElem (a : UInt16Array) (i : USize) (h : i.toNat < a.size) :
a.uget i h = a[i.toNat]
source
@[simp]
theorem ScalarArray.UInt16Array.get!_eq_getElem! (a : UInt16Array) (i : Nat) :
a.get! i = a[i]!
source
@[simp]
theorem ScalarArray.UInt16Array.getD_eq_getD_getElem? (a : UInt16Array) (i : Nat) (v₀ : UInt16) :
a.getD i v₀ = a[i]?.getD v₀
source
@[simp]
theorem ScalarArray.UInt16Array.isEmpty_iff {a : UInt16Array} :
a.isEmpty = true ↔ a = empty

Last element #

source
theorem ScalarArray.UInt16Array.back?_eq_getElem? (a : UInt16Array) :
a.back? = a[a.size - 1]?
source
theorem ScalarArray.UInt16Array.back!_eq_getElem! (a : UInt16Array) :
a.back! = a[a.size - 1]!
source
theorem ScalarArray.UInt16Array.back_eq_getElem (a : UInt16Array) (h : 0 < a.size) :
a.back h = a[a.size - 1]
source
@[simp]
theorem ScalarArray.UInt16Array.getLast?_toList (a : UInt16Array) :
a.toList.getLast? = a.back?
source
@[simp]
theorem ScalarArray.UInt16Array.back?_empty :
empty.back? = none
source
@[simp]
theorem ScalarArray.UInt16Array.back?_push (a : UInt16Array) (v : UInt16) :
(a.push v).back? = some v
source
@[simp]
theorem ScalarArray.UInt16Array.back!_push (a : UInt16Array) (v : UInt16) :
(a.push v).back! = v
source
@[simp]
theorem ScalarArray.UInt16Array.back_push (a : UInt16Array) (v : UInt16) (h : 0 < (a.push v).size) :
(a.push v).back h = v

Writes #

source
@[simp]
theorem ScalarArray.UInt16Array.getElem_uset (a : UInt16Array) (i : USize) (v : UInt16) (h : i.toNat < a.size) (j : Nat) (hj : j < (a.uset i v h).size) :
(a.uset i v h)[j] = if i.toNat = j then v else a[j]
source
@[simp]
theorem ScalarArray.UInt16Array.getElem_set! (a : UInt16Array) (i : Nat) (v : UInt16) (j : Nat) (hj : j < (a.set! i v).size) :
(a.set! i v)[j] = if i = j then v else a[j]
source
@[simp]
theorem ScalarArray.UInt16Array.getElem?_set! (a : UInt16Array) (i : Nat) (v : UInt16) (j : Nat) :
(a.set! i v)[j]? = if i = j then if i < a.size then some v else none else a[j]?
source
theorem ScalarArray.UInt16Array.size_popWhile_le (p : UInt16 → Bool) (a : UInt16Array) :
(popWhile p a).size ≤ a.size
source
@[simp]
theorem ScalarArray.UInt16Array.size_copySlice (src : UInt16Array) (srcOff : Nat) (dest : UInt16Array) (destOff len : Nat) (exact : Bool) :
(src.copySlice srcOff dest destOff len exact).size = max dest.size (min destOff dest.size + min len (src.size - srcOff))
source
theorem ScalarArray.UInt16Array.getElem_copySlice (src : UInt16Array) (srcOff : Nat) (dest : UInt16Array) (destOff len : Nat) (exact : Bool) (i : Nat) (h : i < (src.copySlice srcOff dest destOff len exact).size) :
(src.copySlice srcOff dest destOff len exact)[i] = if h₁ : i < min destOff dest.size then dest[i] else if h₂ : i - min destOff dest.size < min len (src.size - srcOff) then src[srcOff + (i - min destOff dest.size)] else dest[i]

Machine-word indices #

source
theorem ScalarArray.UInt16Array.toNat_usize_of_lt (a : UInt16Array) (h : a.size < USize.size) :
a.usize.toNat = a.size

usize is the size when the size fits in a USize, which holds for every array in memory. Loops over USize indices take this as a hypothesis, since the model Array has no bound on its size.

source
theorem ScalarArray.UInt16Array.lt_usize_iff (a : UInt16Array) (h : a.size < USize.size) {i : USize} :
i < a.usize ↔ i.toNat < a.size

The guard i < a.usize of a loop over USize indices bounds the index.

Folds and queries #

source
@[simp]
theorem ScalarArray.UInt16Array.any_toList (a : UInt16Array) (p : UInt16 → Bool) :
a.toList.any p = a.any p
source
@[simp]
theorem ScalarArray.UInt16Array.all_toList (a : UInt16Array) (p : UInt16 → Bool) :
a.toList.all p = a.all p
source
@[simp]
theorem ScalarArray.UInt16Array.contains_toList (a : UInt16Array) (v : UInt16) :
a.toList.contains v = a.contains v
source
@[simp]
theorem ScalarArray.UInt16Array.foldl_toList {β : Type v} (f : β → UInt16 → β) (init : β) (a : UInt16Array) :
List.foldl f init a.toList = foldl f init a
source
@[simp]
theorem ScalarArray.UInt16Array.foldr_toList {β : Type v} (f : UInt16 → β → β) (init : β) (a : UInt16Array) :
List.foldr f init a.toList = foldr f init a
source
@[simp]
theorem ScalarArray.UInt16Array.forIn_toList {β : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] (a : UInt16Array) (init : β) (f : UInt16 → β → m (ForInStep β)) :
ForIn.forIn a.toList init f = ForIn.forIn a init f
source
theorem ScalarArray.UInt16Array.findIdx?_eq (a : UInt16Array) (p : UInt16 → Bool) (start : Nat) :
a.findIdx? p start = Option.map (fun (x : Nat) => x + start) (List.findIdx? p (List.drop start a.toList))
source
@[simp]
theorem ScalarArray.UInt16Array.findIdx?_toList (a : UInt16Array) (p : UInt16 → Bool) :
List.findIdx? p a.toList = a.findIdx? p
source
@[simp]
theorem ScalarArray.UInt16Array.map_val_findFinIdx? (a : UInt16Array) (p : UInt16 → Bool) (start : Nat) :
Option.map Fin.val (a.findFinIdx? p start) = a.findIdx? p start
source
@[simp]
theorem ScalarArray.UInt16Array.foldlM_toList {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt16 → m β) (init : β) (a : UInt16Array) :
List.foldlM f init a.toList = foldlM f init a
source
@[simp]
theorem ScalarArray.UInt16Array.foldrM_toList {β : Type v} {m : Type v → Type w} [Monad m] (f : UInt16 → β → m β) (init : β) (a : UInt16Array) :
List.foldrM f init a.toList = foldrM f init a
source
@[simp]
theorem ScalarArray.UInt16Array.forM_eq_forM {m : Type v → Type w} [Monad m] (f : UInt16 → m PUnit) (a : UInt16Array) :
forM f a = ForM.forM a f
source
@[simp]
theorem ScalarArray.UInt16Array.forM_toList {m : Type v → Type w} [Monad m] (f : UInt16 → m PUnit) (a : UInt16Array) :
ForM.forM a.toList f = ForM.forM a f

Membership #

source
theorem ScalarArray.UInt16Array.mem_def {x : UInt16} {a : UInt16Array} :
x ∈ a ↔ x ∈ a.toArray
source
@[simp]
theorem ScalarArray.UInt16Array.mem_toArray {x : UInt16} {a : UInt16Array} :
x ∈ a.toArray ↔ x ∈ a
source
@[simp]
theorem ScalarArray.UInt16Array.mem_mk {x : UInt16} {xs : Array UInt16} :
x ∈ mk xs ↔ x ∈ xs
source
@[simp]
theorem ScalarArray.UInt16Array.mem_toList {x : UInt16} {a : UInt16Array} :
x ∈ a.toList ↔ x ∈ a
source
theorem ScalarArray.UInt16Array.mem_iff_getElem {x : UInt16} {a : UInt16Array} :
x ∈ a ↔ ∃ (i : Nat), ∃ (h : i < a.size), a[i] = x
source
theorem ScalarArray.UInt16Array.getElem_mem {a : UInt16Array} {i : Nat} (h : i < a.size) :
a[i] ∈ a
source
@[simp]
theorem ScalarArray.UInt16Array.not_mem_empty (x : UInt16) :
¬x ∈ empty
source
@[simp]
theorem ScalarArray.UInt16Array.mem_push {x v : UInt16} {a : UInt16Array} :
x ∈ a.push v ↔ x ∈ a ∨ x = v
source
@[simp]
theorem ScalarArray.UInt16Array.mem_append {x : UInt16} {a b : UInt16Array} :
x ∈ a ++ b ↔ x ∈ a ∨ x ∈ b

Collecting iterators #

source
@[simp]
theorem Std.Iter.toList_toUInt16Array {α : Type} [Iterator α Id UInt16] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] (it : Iter UInt16) :
it.toUInt16Array.toList = it.toList

Slices #

source
@[simp]
theorem ScalarArray.UInt16Array.Slice.size_copy (s : UInt16Array.Slice) :
s.copy.size = Std.Slice.size s
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.getElem_copy (s : UInt16Array.Slice) (i : Nat) (h : i < s.copy.size) :
s.copy[i] = s[i]
source
@[simp]
theorem ScalarArray.UInt16Array.copy_toSlice (a : UInt16Array) (start stop : Nat) :
(a.toSlice start stop).copy = a.extract start stop

Copying the slice from start to stop is the same as extracting those elements.

source
@[simp]
theorem ScalarArray.UInt16Array.array_toSlice (a : UInt16Array) (start stop : Nat) :
(a.toSlice start stop).array = a
source
@[simp]
theorem ScalarArray.UInt16Array.start_toSlice (a : UInt16Array) (start stop : Nat) :
(a.toSlice start stop).start = min start (min stop a.size)
source
@[simp]
theorem ScalarArray.UInt16Array.stop_toSlice (a : UInt16Array) (start stop : Nat) :
(a.toSlice start stop).stop = min stop a.size
source
@[simp]
theorem ScalarArray.UInt16Array.size_toSlice (a : UInt16Array) (start stop : Nat) :
Std.Slice.size (a.toSlice start stop) = min stop a.size - start
source
@[simp]
theorem ScalarArray.UInt16Array.getElem_toSlice (a : UInt16Array) (start stop i : Nat) (h : i < Std.Slice.size (a.toSlice start stop)) :
(a.toSlice start stop)[i] = a[start + i]
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.size_slice (s : UInt16Array.Slice) (start stop : Nat) :
Std.Slice.size (s.slice start stop) = min stop (Std.Slice.size s) - start
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.getElem_slice (s : UInt16Array.Slice) (start stop i : Nat) (h : i < Std.Slice.size (s.slice start stop)) :
(s.slice start stop)[i] = s[start + i]
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.copy_slice (s : UInt16Array.Slice) (start stop : Nat) :
(s.slice start stop).copy = s.copy.extract start stop
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.array_popFront (s : UInt16Array.Slice) :
s.popFront.array = s.array
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.start_popFront (s : UInt16Array.Slice) :
s.popFront.start = min (s.start + 1) s.stop
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.stop_popFront (s : UInt16Array.Slice) :
s.popFront.stop = s.stop
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.size_popFront (s : UInt16Array.Slice) :
Std.Slice.size s.popFront = Std.Slice.size s - 1
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.getElem_popFront (s : UInt16Array.Slice) (i : Nat) (h : i < Std.Slice.size s.popFront) :
s.popFront[i] = s[i + 1]
source
theorem ScalarArray.UInt16Array.Slice.getD_eq (s : UInt16Array.Slice) (i : Nat) (v₀ : UInt16) :
s.getD i v₀ = if h : i < Std.Slice.size s then s[i] else v₀
source
theorem ScalarArray.UInt16Array.Slice.get!_eq (s : UInt16Array.Slice) (i : Nat) :
s.get! i = if h : i < Std.Slice.size s then s[i] else default
source
theorem ScalarArray.UInt16Array.Slice.foldr_eq_foldr_toList_copy {β : Type v} (f : UInt16 → β → β) (init : β) (s : UInt16Array.Slice) :
foldr f init s = List.foldr f init s.copy.toList

Folding over a slice is folding over the list of its elements.

Slices as copies #

source
@[simp]
theorem ScalarArray.UInt16Array.Slice.size_empty :
Std.Slice.size Slice.empty = 0
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.emptyc_eq_empty :
∅ = Slice.empty
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.copy_empty :
Slice.empty.copy = empty
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.toList_eq_toList_copy (s : UInt16Array.Slice) :
Std.Slice.toList s = s.copy.toList
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.toUInt16Slice_iter (s : UInt16Array.Slice) :
(Std.Slice.iter s).toUInt16Slice = s
source
@[simp]
theorem Std.Iter.iter_toUInt16Slice (it : Iter UInt16) :
Slice.iter it.toUInt16Slice = it
source
theorem Std.Iter.toList_eq_toList_toUInt16Slice (it : Iter UInt16) :
it.toList = Slice.toList it.toUInt16Slice
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.toUInt16Array_iter (s : UInt16Array.Slice) :
(Std.Slice.iter s).toUInt16Array = s.copy
source
@[simp]
theorem ScalarArray.UInt16Array.toUInt16Array_iter (a : UInt16Array) :
a.iter.toUInt16Array = a
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.foldl_eq_foldl_copy {β : Type v} (f : β → UInt16 → β) (init : β) (s : UInt16Array.Slice) :
Std.Slice.foldl f init s = foldl f init s.copy
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.foldlM_eq_foldlM_copy {β : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] (f : β → UInt16 → m β) (init : β) (s : UInt16Array.Slice) :
Std.Slice.foldlM f init s = foldlM f init s.copy
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.forIn_eq_forIn_copy {β : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] (s : UInt16Array.Slice) (init : β) (f : UInt16 → β → m (ForInStep β)) :
ForIn.forIn s init f = ForIn.forIn s.copy init f
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.forM_eq_forM_copy {m : Type v → Type w} [Monad m] [LawfulMonad m] (s : UInt16Array.Slice) (f : UInt16 → m PUnit) :
ForM.forM s f = ForM.forM s.copy f
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.foldr_eq_foldr_copy {β : Type v} (f : UInt16 → β → β) (init : β) (s : UInt16Array.Slice) :
foldr f init s = UInt16Array.foldr f init s.copy
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.foldrM_eq_foldrM_copy {β : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] (f : UInt16 → β → m β) (init : β) (s : UInt16Array.Slice) :
foldrM f init s = UInt16Array.foldrM f init s.copy
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.any_eq_any_copy (s : UInt16Array.Slice) (p : UInt16 → Bool) :
s.any p = s.copy.any p
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.all_eq_all_copy (s : UInt16Array.Slice) (p : UInt16 → Bool) :
s.all p = s.copy.all p
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.contains_eq_contains_copy (s : UInt16Array.Slice) (v : UInt16) :
s.contains v = s.copy.contains v
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.find?_eq_find?_toList_copy (s : UInt16Array.Slice) (p : UInt16 → Bool) :
s.find? p = List.find? p s.copy.toList
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.count_eq_countP_toList_copy (s : UInt16Array.Slice) (p : UInt16 → Bool) :
s.count p = List.countP p s.copy.toList
source
@[simp]
theorem ScalarArray.UInt16Array.Slice.findRev?_eq_find?_reverse_toList_copy (s : UInt16Array.Slice) (p : UInt16 → Bool) :
s.findRev? p = List.find? p s.copy.toList.reverse

Membership in slices #

source
@[simp]
theorem ScalarArray.UInt16Array.Slice.mem_iff_mem_copy {x : UInt16} {s : UInt16Array.Slice} :
x ∈ s ↔ x ∈ s.copy
source
theorem ScalarArray.UInt16Array.Slice.mem_iff_getElem {x : UInt16} {s : UInt16Array.Slice} :
x ∈ s ↔ ∃ (i : Nat), ∃ (h : i < Std.Slice.size s), s[i] = x
source
theorem ScalarArray.UInt16Array.Slice.getElem_mem {s : UInt16Array.Slice} {i : Nat} (h : i < Std.Slice.size s) :
s[i] ∈ s

Slice equality #

source
@[simp]
theorem ScalarArray.UInt16Array.Slice.beq_eq_beq_copy (s t : UInt16Array.Slice) :
(s == t) = (s.copy == t.copy)