Documentation

Mathlib.Data.ByteArray

Main result #

Introduce main properties of Up (well-ordered relation for "upwards" induction on ℕ) and of ByteArray

This entire file has been deprecated on 2024-08-19 in favour of ByteSubarray in Batteries.

source
@[deprecated]
def Nat.Up (ub : Nat) (a : Nat) (i : Nat) :
Prop

A well-ordered relation for "upwards" induction on the natural numbers up to some bound ub.

Equations
  • ub.Up a i = (i < a ∧ i < ub)
source
theorem Nat.Up.next {ub : Nat} {i : Nat} (h : i < ub) :
ub.Up (i + 1) i
source
theorem Nat.Up.WF (ub : Nat) :
WellFounded ub.Up
source
@[deprecated]
def Nat.upRel (ub : Nat) :
WellFoundedRelation Nat

A well-ordered relation for "upwards" induction on the natural numbers up to some bound ub.

Equations
  • ub.upRel = { rel := ub.Up, wf := ⋯ }
source
@[deprecated]
structure ByteSliceT :
Type

A terminal byte slice, a suffix of a byte array.

source
@[inline]
def ByteSliceT.size (self : ByteSliceT) :
Nat

The number of elements in the byte slice.

Equations
  • self.size = self.arr.size - self.off
source
@[inline]
def ByteSliceT.getOp (self : ByteSliceT) (idx : Nat) :
UInt8

Index into a byte slice. The getOp function allows the use of the buf[i] notation.

Equations
  • self.getOp idx = self.arr.get! (self.off + idx)
source
def ByteArray.toSliceT (arr : ByteArray) :
ByteSliceT

Convert a byte array into a terminal slice.

Equations
  • arr.toSliceT = { arr := arr, off := 0 }
source
@[deprecated Batteries.ByteSubarray]
structure ByteSlice :
Type

A byte slice, given by a backing byte array, and an offset and length.

source
def ByteSlice.toArray :
ByteSlice → ByteArray

Convert a byte slice into an array, by copying the data if necessary.

Equations
  • { arr := arr, off := off, len := len }.toArray = arr.extract off len
source
@[inline]
def ByteSlice.getOp (self : ByteSlice) (idx : Nat) :
UInt8

Index into a byte slice. The getOp function allows the use of the buf[i] notation.

Equations
  • self.getOp idx = self.arr.get! (self.off + idx)
source
@[irreducible, deprecated]
def ByteSlice.forIn.loop {m : Type u → Type v} {β : Type u} [Monad m] (f : UInt8 → β → m (ForInStep β)) (arr : ByteArray) (off : Nat) (_end : Nat) (i : Nat) (b : β) :
m β

The inner loop of the forIn implementation for byte slices.

Equations
  • One or more equations did not get rendered due to their size.
source
@[deprecated]
instance ByteSlice.instForInUInt8 {m : Type u → Type v} :
ForIn m ByteSlice UInt8
Equations
  • One or more equations did not get rendered due to their size.
source
def ByteSliceT.toSlice :
ByteSliceT → ByteSlice

Convert a terminal byte slice into a regular byte slice.

Equations
  • { arr := arr, off := off }.toSlice = { arr := arr, off := off, len := arr.size - off }
source
def ByteArray.toSlice (arr : ByteArray) :
ByteSlice

Convert a byte array into a byte slice.

Equations
  • arr.toSlice = { arr := arr, off := 0, len := arr.size }
source
def ByteSlice.toString (bs : ByteSlice) :
String

Convert a byte slice into a string. This does not handle non-ASCII characters correctly: every byte will become a unicode character with codepoint < 256.

Equations
  • One or more equations did not get rendered due to their size.
source
instance instToStringByteSlice :
ToString ByteSlice
Equations
  • One or more equations did not get rendered due to their size.