def ByteArray.instBEq.beq : ByteArray → ByteArray → Bool

@[implicit_reducible]

instance ByteArray.instBEq : BEq ByteArray

theorem ByteArray.ext_iff {x y : ByteArray} : x = y ↔ x.data = y.data

@[implicit_reducible]

instance ByteArray.instDecidableEq : DecidableEq ByteArray

@[implicit_reducible]

instance ByteArray.instInhabited : Inhabited ByteArray

@[implicit_reducible]

instance ByteArray.instEmptyCollection : EmptyCollection ByteArray

@[extern lean_sarray_size]

def ByteArray.usize (a : ByteArray) : USize

Retrieves the size of the array as a platform-specific fixed-width integer.

Because USize is big enough to address all memory on every platform that Lean supports, there are in practice no ByteArrays that have more elements that USize can count.

@[extern lean_byte_array_uget]

def ByteArray.uget (a : ByteArray) (i : USize) (h : i.toNat < a.size := by get_elem_tactic) : UInt8

Retrieves the byte at the indicated index. Callers must prove that the index is in bounds. The index is represented by a platform-specific fixed-width integer (either 32 or 64 bits).

Because USize is big enough to address all memory on every platform that Lean supports, there are in practice no ByteArrays for which uget cannot retrieve all elements.

@[extern lean_byte_array_get]

def ByteArray.get! : ByteArray → Nat → UInt8

Retrieves the byte at the indicated index. Panics if the index is out of bounds.

@[extern lean_byte_array_fget]

def ByteArray.get (a : ByteArray) (i : Nat) (h : i < a.size := by get_elem_tactic) : UInt8

Retrieves the byte at the indicated index. Callers must prove that the index is in bounds.

Use uget for a more efficient alternative or get! for a variant that panics if the index is out of bounds.

@[implicit_reducible]

instance ByteArray.instGetElemNatUInt8LtSize : GetElem ByteArray Nat UInt8 fun (xs : ByteArray) (i : Nat) => i < xs.size

@[implicit_reducible]

instance ByteArray.instGetElemUSizeUInt8LtNatValToFinSize : GetElem ByteArray USize UInt8 fun (xs : ByteArray) (i : USize) => ↑i.toFin < xs.size

@[extern lean_byte_array_set]

def ByteArray.set! : ByteArray → Nat → UInt8 → ByteArray

Replaces the byte at the given index.

The array is modified in-place if there are no other references to it.

If the index is out of bounds, the array is returned unmodified.

@[extern lean_byte_array_fset]

def ByteArray.set (a : ByteArray) (i : Nat) : UInt8 → (h : autoParam (i < a.size) set._auto_1) → ByteArray

Replaces the byte at the given index.

No bounds check is performed, but the function requires a proof that the index is in bounds. This proof can usually be omitted, and will be synthesized automatically.

The array is modified in-place if there are no other references to it.

@[extern lean_byte_array_uset]

def ByteArray.uset (a : ByteArray) (i : USize) : UInt8 → (h : autoParam (i.toNat < a.size) uset._auto_1) → ByteArray

Replaces the byte at the given index.

No bounds check is performed, but the function requires a proof that the index is in bounds. This proof can usually be omitted, and will be synthesized automatically.

The array is modified in-place if there are no other references to it.

@[extern lean_byte_array_hash]

opaque ByteArray.hash (a : ByteArray) : UInt64

Computes a hash for a ByteArray.

@[implicit_reducible]

instance ByteArray.instHashable : Hashable ByteArray

def ByteArray.isEmpty (s : ByteArray) : Bool

Returns true when s contains zero bytes.

@[extern lean_byte_array_copy_slice]

def ByteArray.copySlice (src : ByteArray) (srcOff : Nat) (dest : ByteArray) (destOff len : Nat) (exact : Bool := true) : ByteArray

Copies the slice at [srcOff, srcOff + len) in src to [destOff, destOff + len) in dest, growing dest if necessary. If exact is false, the capacity will be doubled when grown.

def ByteArray.extract (a : ByteArray) (b e : Nat) : ByteArray

Copies the bytes with indices b (inclusive) to e (exclusive) to a new ByteArray.

@[inline]

def ByteArray.fastAppend (a b : ByteArray) : ByteArray

Appends two byte arrays using fast array primitives instead of converting them into lists and back.

In compiled code, this function replaces calls to ByteArray.append.

@[simp]

theorem ByteArray.size_data {a : ByteArray} : a.data.size = a.size

@[csimp]

theorem ByteArray.append_eq_fastAppend : ByteArray.append = ByteArray.fastAppend

@[implicit_reducible]

instance ByteArray.instAppend : Append ByteArray

@[simp]

theorem ByteArray.append_eq {a b : ByteArray} : a.append b = a ++ b

@[simp]

theorem ByteArray.fastAppend_eq {a b : ByteArray} : a.fastAppend b = a ++ b

def ByteArray.toList (bs : ByteArray) : List UInt8

Converts a packed array of bytes to a linked list.

@[irreducible]

def ByteArray.toList.loop (bs : ByteArray) (i : Nat) (r : List UInt8) : List UInt8

@[inline]

def ByteArray.findFinIdx? (a : ByteArray) (p : UInt8 → Bool) (start : Nat := 0) : Option (Fin a.size)

Finds the index of the first byte in a for which p returns true. If no byte in a satisfies p, then the result is none.

The index is returned along with a proof that it is a valid index in the array.

@[irreducible, specialize #[]]

def ByteArray.findFinIdx?.loop (a : ByteArray) (p : UInt8 → Bool) (i : Nat) : Option (Fin a.size)

@[inline]

def ByteArray.findIdx? (a : ByteArray) (p : UInt8 → Bool) (start : Nat := 0) : Option Nat

Finds the index of the first byte in a for which p returns true. If no byte in a satisfies p, then the result is none.

The variant findFinIdx? additionally returns a proof that the found index is in bounds.

@[irreducible, specialize #[]]

def ByteArray.findIdx?.loop (a : ByteArray) (p : UInt8 → Bool) (i : Nat) : Option Nat

@[inline]

unsafe def ByteArray.forInUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteArray) (b : β) (f : UInt8 → β → m (ForInStep β)) : m β

An efficient implementation of ForIn.forIn for ByteArray that uses USize rather than Nat for indices.

We claim this unsafe implementation is correct because an array cannot have more than USize.size elements in our runtime. This is similar to the Array version.

@[specialize #[]]

unsafe def ByteArray.forInUnsafe.loop {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteArray) (f : UInt8 → β → m (ForInStep β)) (sz i : USize) (b : β) : m β

@[implemented_by ByteArray.forInUnsafe]

def ByteArray.forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteArray) (b : β) (f : UInt8 → β → m (ForInStep β)) : m β

The reference implementation of ForIn.forIn for ByteArray.

In compiled code, this is replaced by the more efficient ByteArray.forInUnsafe.

def ByteArray.forIn.loop {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteArray) (f : UInt8 → β → m (ForInStep β)) (i : Nat) (h : i ≤ as.size) (b : β) : m β

@[implicit_reducible]

instance ByteArray.instForInUInt8OfMonad {m : Type u_1 → Type u_2} [Monad m] : ForIn m ByteArray UInt8

@[inline]

unsafe def ByteArray.foldlMUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 → m β) (init : β) (as : ByteArray) (start : Nat := 0) (stop : Nat := as.size) : m β

An efficient implementation of a monadic left fold on for ByteArray that uses USize rather than Nat for indices.

We claim this unsafe implementation is correct because an array cannot have more than USize.size elements in our runtime. This is similar to the Array version.

@[specialize #[]]

unsafe def ByteArray.foldlMUnsafe.fold {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 → m β) (as : ByteArray) (i stop : USize) (b : β) : m β

@[implemented_by ByteArray.foldlMUnsafe]

def ByteArray.foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 → m β) (init : β) (as : ByteArray) (start : Nat := 0) (stop : Nat := as.size) : m β

A monadic left fold on ByteArray that iterates over an array from low to high indices, computing a running value.

Each element of the array is combined with the value from the prior elements using a monadic function f. The initial value init is the starting value before any elements have been processed.

def ByteArray.foldlM.loop {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 → m β) (as : ByteArray) (stop : Nat) (h : stop ≤ as.size) (i j : Nat) (b : β) : m β

@[inline]

def ByteArray.foldl {β : Type v} (f : β → UInt8 → β) (init : β) (as : ByteArray) (start : Nat := 0) (stop : Nat := as.size) : β

A left fold on ByteArray that iterates over an array from low to high indices, computing a running value.

Each element of the array is combined with the value from the prior elements using a function f. The initial value init is the starting value before any elements have been processed.

ByteArray.foldlM is a monadic variant of this function.

structure ByteArray.Iterator : Type

Iterator over the bytes (UInt8) of a ByteArray.

Typically created by arr.iter, where arr is a ByteArray.

An iterator is valid if the position i is valid for the array arr, meaning 0 ≤ i ≤ arr.size

Most operations on iterators return arbitrary values if the iterator is not valid. The functions in the ByteArray.Iterator API should rule out the creation of invalid iterators, with two exceptions:

• Iterator.next iter is invalid if iter is already at the end of the array (iter.atEnd is true)
• Iterator.forward iter n/Iterator.nextn iter n is invalid if n is strictly greater than the number of remaining bytes.

• array : ByteArray

  The array the iterator is for.

• idx : Nat

  The current position.

  This position is not necessarily valid for the array, for instance if one keeps calling Iterator.next when Iterator.atEnd is true. If the position is not valid, then the current byte is (default : UInt8).

@[implicit_reducible]

instance ByteArray.instInhabitedIterator : Inhabited Iterator

def ByteArray.instInhabitedIterator.default : Iterator

def ByteArray.mkIterator (arr : ByteArray) : Iterator

Creates an iterator at the beginning of an array.

@[reducible, inline]

abbrev ByteArray.iter (arr : ByteArray) : Iterator

Creates an iterator at the beginning of an array.

@[implicit_reducible]

instance ByteArray.instSizeOfIterator : SizeOf Iterator

The size of an array iterator is the number of bytes remaining.

theorem ByteArray.Iterator.sizeOf_eq (i : Iterator) : sizeOf i = i.array.size - i.idx

def ByteArray.Iterator.remainingBytes : Iterator → Nat

The number of bytes remaining in the iterator.

def ByteArray.Iterator.pos (self : Iterator) : Nat

The current position.

This position is not necessarily valid for the array, for instance if one keeps calling Iterator.next when Iterator.atEnd is true. If the position is not valid, then the current byte is (default : UInt8).

@[inline]

def ByteArray.Iterator.atEnd : Iterator → Bool

True if the iterator is past the array's last byte.

@[inline]

def ByteArray.Iterator.curr : Iterator → UInt8

The byte at the current position.

On an invalid position, returns (default : UInt8).

@[inline]

def ByteArray.Iterator.next : Iterator → Iterator

Moves the iterator's position forward by one byte, unconditionally.

It is only valid to call this function if the iterator is not at the end of the array, i.e. Iterator.atEnd is false; otherwise, the resulting iterator will be invalid.

@[inline]

def ByteArray.Iterator.prev : Iterator → Iterator

Decreases the iterator's position.

If the position is zero, this function is the identity.

@[inline]

def ByteArray.Iterator.hasNext : Iterator → Bool

True if the iterator is valid; that is, it is not past the array's last byte.

@[inline]

def ByteArray.Iterator.curr' (it : Iterator) (h : it.hasNext = true) : UInt8

The byte at the current position. -

@[inline]

def ByteArray.Iterator.next' (it : Iterator) (_h : it.hasNext = true) : Iterator

Moves the iterator's position forward by one byte. -

@[inline]

def ByteArray.Iterator.hasPrev : Iterator → Bool

True if the position is not zero.

@[inline]

def ByteArray.Iterator.toEnd : Iterator → Iterator

Moves the iterator's position to the end of the array.

Given i : ByteArray.Iterator, note that i.toEnd.atEnd is always true.

@[inline]

def ByteArray.Iterator.forward : Iterator → Nat → Iterator

Moves the iterator's position several bytes forward.

The resulting iterator is only valid if the number of bytes to skip is less than or equal to the number of bytes left in the iterator.

@[inline]

def ByteArray.Iterator.nextn : Iterator → Nat → Iterator

Moves the iterator's position several bytes forward.

The resulting iterator is only valid if the number of bytes to skip is less than or equal to the number of bytes left in the iterator.

@[inline]

def ByteArray.Iterator.prevn : Iterator → Nat → Iterator

Moves the iterator's position several bytes back.

If asked to go back more bytes than available, stops at the beginning of the array.

@[implicit_reducible]

instance instToStringByteArray : ToString ByteArray