Documentation

Mathlib.Data.ByteArray

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

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)
Instances For
    theorem Nat.Up.next {ub : Nat} {i : Nat} (h : i < ub) :
    ub.Up (i + 1) i
    theorem Nat.Up.WF (ub : Nat) :

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

    Equations
    • ub.upRel = { rel := ub.Up, wf := }
    Instances For
      structure ByteSliceT :

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

      Instances For
        @[inline]

        The number of elements in the byte slice.

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

          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)
          Instances For

            Convert a byte array into a terminal slice.

            Equations
            • arr.toSliceT = { arr := arr, off := 0 }
            Instances For
              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
                • x.toArray = match x with | { arr := arr, off := off, len := len } => arr.extract off len
                Instances For
                  @[inline]
                  def ByteSlice.getOp (self : ByteSlice) (idx : Nat) :

                  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)
                  Instances For
                    @[irreducible]
                    def ByteSlice.forIn.loop {m : Type u_1 → Type u_2} {β : Type u_1} [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.
                    Instances For
                      instance ByteSlice.instForInUInt8 {m : Type u_1 → Type u_2} :
                      Equations
                      • One or more equations did not get rendered due to their size.

                      Convert a terminal byte slice into a regular byte slice.

                      Equations
                      • x.toSlice = match x with | { arr := arr, off := off } => { arr := arr, off := off, len := arr.size - off }
                      Instances For

                        Convert a byte array into a byte slice.

                        Equations
                        • arr.toSlice = { arr := arr, off := 0, len := arr.size }
                        Instances For

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

                          Equations
                          Instances For
                            @[irreducible]
                            Equations
                            Instances For

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