Documentation

Batteries.Data.ByteArray

source
theorem ByteArray.ext {a : ByteArray} {b : ByteArray} :
a.data = b.data → a = b
source
theorem ByteArray.getElem_eq_data_getElem {i : Nat} (a : ByteArray) (h : i < a.size) :
a[i] = a.data[i]

uget/uset #

source
@[simp]
theorem ByteArray.uset_eq_set (a : ByteArray) {i : USize} (h : i.toNat < a.size) (v : UInt8) :
a.uset i v h = a.set ⟨i.toNat, h⟩ v

empty #

source
@[simp]
theorem ByteArray.mkEmpty_data (cap : Nat) :
(ByteArray.mkEmpty cap).data = #[]
source
@[simp]
theorem ByteArray.empty_data :
ByteArray.empty.data = #[]
source
@[simp]
theorem ByteArray.size_empty :
ByteArray.empty.size = 0

push #

source
@[simp]
theorem ByteArray.push_data (a : ByteArray) (b : UInt8) :
(a.push b).data = a.data.push b
source
@[simp]
theorem ByteArray.size_push (a : ByteArray) (b : UInt8) :
(a.push b).size = a.size + 1
source
@[simp]
theorem ByteArray.get_push_eq (a : ByteArray) (x : UInt8) :
(a.push x)[a.size] = x
source
theorem ByteArray.get_push_lt (a : ByteArray) (x : UInt8) (i : Nat) (h : i < a.size) :
(a.push x)[i] = a[i]

set #

source
@[simp]
theorem ByteArray.set_data (a : ByteArray) (i : Fin a.size) (v : UInt8) :
(a.set i v).data = a.data.set i v
source
@[simp]
theorem ByteArray.size_set (a : ByteArray) (i : Fin a.size) (v : UInt8) :
(a.set i v).size = a.size
source
@[simp]
theorem ByteArray.get_set_eq (a : ByteArray) (i : Fin a.size) (v : UInt8) :
(a.set i v)[↑i] = v
source
theorem ByteArray.get_set_ne {j : Nat} (a : ByteArray) (i : Fin a.size) (v : UInt8) (hj : j < a.size) (h : ↑i ≠ j) :
(a.set i v)[j] = a[j]
source
theorem ByteArray.set_set (a : ByteArray) (i : Fin a.size) (v : UInt8) (v' : UInt8) :
(a.set i v).set ⟨↑i, ⋯⟩ v' = a.set i v'

copySlice #

source
@[simp]
theorem ByteArray.copySlice_data (a : ByteArray) (i : Nat) (b : ByteArray) (j : Nat) (len : Nat) (exact : Bool) :
(a.copySlice i b j len exact).data = b.data.extract 0 j ++ a.data.extract i (i + len) ++ b.data.extract (j + min len (a.data.size - i)) b.data.size

append #

source
@[simp]
theorem ByteArray.append_eq (a : ByteArray) (b : ByteArray) :
a.append b = a ++ b
source
@[simp]
theorem ByteArray.append_data (a : ByteArray) (b : ByteArray) :
(a ++ b).data = a.data ++ b.data
source
theorem ByteArray.size_append (a : ByteArray) (b : ByteArray) :
(a ++ b).size = a.size + b.size
source
theorem ByteArray.get_append_left {i : Nat} {a : ByteArray} {b : ByteArray} (hlt : i < a.size) (h : optParam (i < (a ++ b).size) ⋯) :
(a ++ b)[i] = a[i]
source
theorem ByteArray.get_append_right {i : Nat} {a : ByteArray} {b : ByteArray} (hle : a.size ≤ i) (h : i < (a ++ b).size) (h' : optParam (i - a.size < b.size) ⋯) :
(a ++ b)[i] = b[i - a.size]

extract #

source
@[simp]
theorem ByteArray.extract_data (a : ByteArray) (start : Nat) (stop : Nat) :
(a.extract start stop).data = a.data.extract start stop
source
@[simp]
theorem ByteArray.size_extract (a : ByteArray) (start : Nat) (stop : Nat) :
(a.extract start stop).size = min stop a.size - start
source
theorem ByteArray.get_extract_aux {i : Nat} {a : ByteArray} {start : Nat} {stop : Nat} (h : i < (a.extract start stop).size) :
start + i < a.size
source
@[simp]
theorem ByteArray.get_extract {i : Nat} {a : ByteArray} {start : Nat} {stop : Nat} (h : i < (a.extract start stop).size) :
(a.extract start stop)[i] = a[start + i]

ofFn #

source
def ByteArray.ofFn {n : Nat} (f : Fin n → UInt8) :
ByteArray
  • ofFn f with f : Fin n → UInt8 returns the byte array whose ith element is f i. -
Equations
Instances For
    source
    @[simp]
    theorem ByteArray.ofFn_data {n : Nat} (f : Fin n → UInt8) :
    (ByteArray.ofFn f).data = Array.ofFn f
    source
    @[simp]
    theorem ByteArray.size_ofFn {n : Nat} (f : Fin n → UInt8) :
    (ByteArray.ofFn f).size = n
    source
    @[simp]
    theorem ByteArray.get_ofFn {n : Nat} (f : Fin n → UInt8) (i : Fin (ByteArray.ofFn f).size) :
    (ByteArray.ofFn f).get i = f (Fin.cast ⋯ i)
    source
    @[simp]
    theorem ByteArray.getElem_ofFn {n : Nat} (f : Fin n → UInt8) (i : Nat) (h : i < (ByteArray.ofFn f).size) :
    (ByteArray.ofFn f)[i] = f ⟨i, ⋯⟩