Documentation

Batteries.Data.ByteArray

source
@[instance_reducible]
instance ByteArray.instDecidableEq_batteries :
DecidableEq ByteArray
Equations
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 v h

empty #

source
@[simp]
theorem ByteArray.data_mkEmpty (cap : Nat) :
(emptyWithCapacity cap).data = #[]

push #

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.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 v' : UInt8) :
(a.set (↑i) v ⋯).set (↑i) v' ⋯ = a.set (↑i) v' ⋯

copySlice #

source
@[simp]
theorem ByteArray.data_copySlice (a : ByteArray) (i : Nat) (b : ByteArray) (j 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))

append #

source
theorem ByteArray.get_append_left {i : Nat} {a b : ByteArray} (hlt : i < a.size) (h : i < (a ++ b).size := ⋯) :
(a ++ b)[i] = a[i]
source
theorem ByteArray.get_append_right {i : Nat} {a b : ByteArray} (hle : a.size ≤ i) (h : i < (a ++ b).size) (h' : i - a.size < b.size := ⋯) :
(a ++ b)[i] = b[i - a.size]

extract #

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

ofFn #

source
@[inline]
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_zero (f : Fin 0 → UInt8) :
    ofFn f = empty
    source
    theorem ByteArray.ofFn_succ {n : Nat} (f : Fin (n + 1) → UInt8) :
    ofFn f = (ofFn fun (i : Fin n) => f i.castSucc).push (f (Fin.last n))
    source
    @[simp]
    theorem ByteArray.data_ofFn {n : Nat} (f : Fin n → UInt8) :
    (ofFn f).data = Array.ofFn f
    source
    @[simp]
    theorem ByteArray.size_ofFn {n : Nat} (f : Fin n → UInt8) :
    (ofFn f).size = n
    source
    @[simp]
    theorem ByteArray.get_ofFn {n : Nat} (f : Fin n → UInt8) (i : Fin (ofFn f).size) :
    (ofFn f).get ↑i ⋯ = f (Fin.cast ⋯ i)
    source
    @[simp]
    theorem ByteArray.getElem_ofFn {n : Nat} (f : Fin n → UInt8) (i : Nat) (h : i < (ofFn f).size) :
    (ofFn f)[i] = f ⟨i, ⋯⟩

    map/mapM #

    source
    @[inline]
    unsafe def ByteArray.mapMUnsafe {m : Type → Type u_1} [Monad m] (a : ByteArray) (f : UInt8 → m UInt8) :
    m ByteArray

    Unsafe optimized implementation of mapM.

    This function is unsafe because it relies on the implementation limit that the size of an array is always less than USize.size.

    Equations
    Instances For
      source
      @[implemented_by ByteArray.mapMUnsafe]
      def ByteArray.mapM {m : Type → Type u_1} [Monad m] (a : ByteArray) (f : UInt8 → m UInt8) :
      m ByteArray

      mapM f a applies the monadic function f to each element of the array.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[inline]
        def ByteArray.map (a : ByteArray) (f : UInt8 → UInt8) :
        ByteArray

        map f a applies the function f to each element of the array.

        Equations
        Instances For