source
@[simp]
theorem emptyc_eq_empty :
∅ = ByteArray.empty
source
@[simp]
theorem emptyWithCapacity_eq_empty :
ByteArray.emptyWithCapacity 0 = ByteArray.empty
source
@[simp]
theorem ByteArray.data_empty :
empty.data = #[]
source
@[simp]
theorem ByteArray.data_extract {a : ByteArray} {b e : Nat} :
(a.extract b e).data = a.data.extract b e
source
@[simp]
theorem ByteArray.extract_zero_size {b : ByteArray} :
b.extract 0 b.size = b
source
@[simp]
theorem ByteArray.extract_same {b : ByteArray} {i : Nat} :
b.extract i i = empty
source
theorem ByteArray.fastAppend_eq_copySlice {a b : ByteArray} :
a.fastAppend b = b.copySlice 0 a a.size b.size false
source
@[simp]
theorem List.toByteArray_append {l l' : List UInt8} :
(l ++ l').toByteArray = l.toByteArray ++ l'.toByteArray
source
@[simp]
theorem ByteArray.toList_data_append {l l' : ByteArray} :
(l ++ l').data.toList = l.data.toList ++ l'.data.toList
source
@[simp]
theorem ByteArray.data_append {l l' : ByteArray} :
(l ++ l').data = l.data ++ l'.data
source
@[simp]
theorem ByteArray.size_empty :
empty.size = 0
source
@[simp]
theorem List.data_toByteArray {l : List UInt8} :
l.toByteArray.data = l.toArray
source
@[simp]
theorem List.size_toByteArray {l : List UInt8} :
l.toByteArray.size = l.length
source
@[simp]
theorem List.toByteArray_nil :
[].toByteArray = ByteArray.empty
source
@[simp]
theorem ByteArray.empty_append {b : ByteArray} :
empty ++ b = b
source
@[simp]
theorem ByteArray.append_empty {b : ByteArray} :
b ++ empty = b
source
@[simp]
theorem ByteArray.size_append {a b : ByteArray} :
(a ++ b).size = a.size + b.size
source
@[simp]
theorem ByteArray.size_eq_zero_iff {a : ByteArray} :
a.size = 0 ↔ a = empty
source
theorem ByteArray.getElem_eq_getElem_data {a : ByteArray} {i : Nat} {h : i < a.size} :
a[i] = a.data[i]
source
@[simp]
theorem ByteArray.getElem_append_left {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size} (hlt : i < a.size) :
(a ++ b)[i] = a[i]
source
theorem ByteArray.getElem_append_right {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size} (hle : a.size ≤ i) :
(a ++ b)[i] = b[i - a.size]
source
@[simp]
theorem List.getElem_toByteArray {l : List UInt8} {i : Nat} {h : i < l.toByteArray.size} :
l.toByteArray[i] = l[i]
source
theorem List.getElem_eq_getElem_toByteArray {l : List UInt8} {i : Nat} {h : i < l.length} :
l[i] = l.toByteArray[i]
source
@[simp]
theorem ByteArray.size_extract {a : ByteArray} {b e : Nat} :
(a.extract b e).size = min e a.size - b
source
@[simp]
theorem ByteArray.extract_eq_empty_iff {b : ByteArray} {i j : Nat} :
b.extract i j = empty ↔ min j b.size ≤ i
source
@[simp]
theorem ByteArray.extract_add_left {b : ByteArray} {i j : Nat} :
b.extract (i + j) i = empty
source
@[simp]
theorem ByteArray.append_eq_empty_iff {a b : ByteArray} :
a ++ b = empty ↔ a = empty ∧ b = empty
source
@[simp]
theorem List.toByteArray_eq_empty {l : List UInt8} :
l.toByteArray = ByteArray.empty ↔ l = []
source
theorem ByteArray.append_right_inj {ys₁ ys₂ : ByteArray} (xs : ByteArray) :
xs ++ ys₁ = xs ++ ys₂ ↔ ys₁ = ys₂
source
@[simp]
theorem ByteArray.extract_append_extract {a : ByteArray} {i j k : Nat} :
a.extract i j ++ a.extract j k = a.extract (min i j) (max j k)
source
theorem ByteArray.extract_eq_extract_append_extract {a : ByteArray} {i k : Nat} (j : Nat) (hi : i ≤ j) (hk : j ≤ k) :
a.extract i k = a.extract i j ++ a.extract j k
source
theorem ByteArray.append_inj_left {xs₁ xs₂ ys₁ ys₂ : ByteArray} (h : xs₁ ++ ys₁ = xs₂ ++ ys₂) (hl : xs₁.size = xs₂.size) :
xs₁ = xs₂
source
theorem ByteArray.extract_append_eq_right {a b : ByteArray} {i j : Nat} (hi : i = a.size) (hj : j = a.size + b.size) :
(a ++ b).extract i j = b
source
theorem ByteArray.extract_append_eq_left {a b : ByteArray} {i : Nat} (hi : i = a.size) :
(a ++ b).extract 0 i = a
source
theorem ByteArray.extract_append_size_left {a b : ByteArray} {i : Nat} :
(a ++ b).extract i a.size = a.extract i a.size
source
theorem ByteArray.extract_append_size_add {a b : ByteArray} {i j : Nat} :
(a ++ b).extract (a.size + i) (a.size + j) = b.extract i j
source
theorem ByteArray.extract_append {as bs : ByteArray} {i j : Nat} :
(as ++ bs).extract i j = as.extract i j ++ bs.extract (i - as.size) (j - as.size)
source
theorem ByteArray.extract_append_size_add' {a b : ByteArray} {i j k : Nat} (h : k = a.size) :
(a ++ b).extract (k + i) (k + j) = b.extract i j
source
theorem ByteArray.extract_extract {a : ByteArray} {i j k l : Nat} :
(a.extract i j).extract k l = a.extract (i + k) (min (i + l) j)
source
theorem ByteArray.getElem_extract_aux {i : Nat} {xs : ByteArray} {start stop : Nat} (h : i < (xs.extract start stop).size) :
start + i < xs.size
source
theorem ByteArray.getElem_extract {i : Nat} {b : ByteArray} {start stop : Nat} (h : i < (b.extract start stop).size) :
(b.extract start stop)[i] = b[start + i]
source
theorem ByteArray.extract_eq_extract_left {a : ByteArray} {i i' j : Nat} :
a.extract i j = a.extract i' j ↔ min j a.size - i = min j a.size - i'
source
theorem ByteArray.extract_add_one {a : ByteArray} {i : Nat} (ha : i + 1 ≤ a.size) :
a.extract i (i + 1) = [a[i]].toByteArray
source
theorem ByteArray.extract_add_two {a : ByteArray} {i : Nat} (ha : i + 2 ≤ a.size) :
a.extract i (i + 2) = [a[i], a[i + 1]].toByteArray
source
theorem ByteArray.extract_add_three {a : ByteArray} {i : Nat} (ha : i + 3 ≤ a.size) :
a.extract i (i + 3) = [a[i], a[i + 1], a[i + 2]].toByteArray
source
theorem ByteArray.extract_add_four {a : ByteArray} {i : Nat} (ha : i + 4 ≤ a.size) :
a.extract i (i + 4) = [a[i], a[i + 1], a[i + 2], a[i + 3]].toByteArray
source
theorem ByteArray.append_assoc {a b c : ByteArray} :
a ++ b ++ c = a ++ (b ++ c)
source
@[simp]
theorem ByteArray.toList_empty :
empty.toList = []
source
theorem ByteArray.copySlice_eq_append {src : ByteArray} {srcOff : Nat} {dest : ByteArray} {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.data.size - srcOff)) dest.data.size
source
@[simp]
theorem ByteArray.data_set {as : ByteArray} {i : Nat} {h : i < as.size} {a : UInt8} :
(as.set i a h).data = as.data.set i a ⋯
source
theorem ByteArray.set_eq_push_extract_append_extract {as : ByteArray} {i : Nat} (h : i < as.size) {a : UInt8} :
as.set i a h = (as.extract 0 i).push a ++ as.extract (i + 1) as.size
source
@[simp]
theorem ByteArray.append_toByteArray_singleton {as : ByteArray} {a : UInt8} :
as ++ [a].toByteArray = as.push a