Documentation

Mathlib.Data.ByteArray

def Nat.Up (ub : ) (a : ) (i : ) :

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

Equations
theorem Nat.Up.next {ub : } {i : } (h : i < ub) :
Nat.Up ub (i + 1) i

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

Equations
structure ByteSliceT :

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

Instances For
    @[inline]

    The number of elements in the byte slice.

    Equations
    @[inline]
    def ByteSliceT.getOp (self : ByteSliceT) (idx : ) :

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

    Equations

    Convert a byte array into a terminal slice.

    Equations
    structure ByteSlice :

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

    Instances For

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

      Equations
      @[inline]
      def ByteSlice.getOp (self : ByteSlice) (idx : ) :

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

      Equations
      def ByteSlice.forIn.loop {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] (f : UInt8βm (ForInStep β)) (arr : ByteArray) (off : ) (_end : ) (i : ) (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.
      Equations
      • One or more equations did not get rendered due to their size.

      Convert a terminal byte slice into a regular byte slice.

      Equations

      Convert a byte array into a byte slice.

      Equations

      Convert a string of assumed-ASCII characters into a byte array. (If any characters are non-ASCII they will be reduced modulo 256.)

      Equations
      Equations
      • One or more equations did not get rendered due to their size.

      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.
      Equations
      • One or more equations did not get rendered due to their size.