Documentation

Init.Data.ByteArray.Basic

structure ByteArray :
Instances For
    @[extern lean_mk_empty_byte_array]
    Equations
    Instances For
      @[extern lean_byte_array_push]
      Equations
      • x✝.push x = match x✝, x with | { data := bs }, b => { data := bs.push b }
      Instances For
        @[extern lean_byte_array_size]
        Equations
        • x.size = match x with | { data := bs } => bs.size
        Instances For
          @[extern lean_byte_array_uget]
          def ByteArray.uget (a : ByteArray) (i : USize) :
          i.toNat < a.sizeUInt8
          Equations
          • x✝¹.uget x✝ x = match x✝¹, x✝, x with | { data := bs }, i, h => bs[i]
          Instances For
            @[extern lean_byte_array_get]
            Equations
            • x✝.get! x = match x✝, x with | { data := bs }, i => bs.get! i
            Instances For
              @[extern lean_byte_array_fget]
              def ByteArray.get (a : ByteArray) :
              Fin a.sizeUInt8
              Equations
              • x✝.get x = match x✝, x with | { data := bs }, i => bs.get i
              Instances For
                Equations
                Equations
                @[extern lean_byte_array_set]
                Equations
                • x✝¹.set! x✝ x = match x✝¹, x✝, x with | { data := bs }, i, b => { data := bs.set! i b }
                Instances For
                  @[extern lean_byte_array_fset]
                  def ByteArray.set (a : ByteArray) :
                  Fin a.sizeUInt8ByteArray
                  Equations
                  • x✝¹.set x✝ x = match x✝¹, x✝, x with | { data := bs }, i, b => { data := bs.set i b }
                  Instances For
                    @[extern lean_byte_array_uset]
                    def ByteArray.uset (a : ByteArray) (i : USize) :
                    UInt8i.toNat < a.sizeByteArray
                    Equations
                    • x✝².uset x✝¹ x✝ x = match x✝², x✝¹, x✝, x with | { data := bs }, i, v, h => { data := bs.uset i v h }
                    Instances For
                      @[extern lean_byte_array_hash]
                      Equations
                      • s.isEmpty = (s.size == 0)
                      Instances For
                        @[extern lean_byte_array_copy_slice]
                        def ByteArray.copySlice (src : ByteArray) (srcOff : Nat) (dest : ByteArray) (destOff : Nat) (len : Nat) (exact : optParam Bool true) :

                        Copy 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.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Equations
                          Instances For
                            Equations
                            • a.append b = b.copySlice 0 a a.size b.size false
                            Instances For
                              Equations
                              Instances For
                                partial def ByteArray.toList.loop (bs : ByteArray) (i : Nat) (r : List UInt8) :
                                @[inline]
                                def ByteArray.findIdx? (a : ByteArray) (p : UInt8Bool) (start : optParam Nat 0) :
                                Equations
                                Instances For
                                  @[specialize #[]]
                                  partial def ByteArray.findIdx?.loop (a : ByteArray) (p : UInt8Bool) (i : Nat) :
                                  @[inline]
                                  unsafe def ByteArray.forInUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteArray) (b : β) (f : UInt8βm (ForInStep β)) :
                                  m β

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

                                  TODO: avoid code duplication in the future after we improve the compiler.

                                  Equations
                                  Instances For
                                    @[specialize #[]]
                                    unsafe def ByteArray.forInUnsafe.loop {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteArray) (f : UInt8βm (ForInStep β)) (sz : USize) (i : USize) (b : β) :
                                    m β
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[implemented_by ByteArray.forInUnsafe]
                                      def ByteArray.forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteArray) (b : β) (f : UInt8βm (ForInStep β)) :
                                      m β

                                      Reference implementation for forIn

                                      Equations
                                      Instances For
                                        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 β
                                        Equations
                                        Instances For
                                          instance ByteArray.instForInUInt8 {m : Type u_1 → Type u_2} :
                                          Equations
                                          • ByteArray.instForInUInt8 = { forIn := fun {β : Type u_1} [Monad m] => ByteArray.forIn }
                                          @[inline]
                                          unsafe def ByteArray.foldlMUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (f : βUInt8m β) (init : β) (as : ByteArray) (start : optParam Nat 0) (stop : optParam Nat as.size) :
                                          m β

                                          See comment at forInUnsafe

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            @[specialize #[]]
                                            unsafe def ByteArray.foldlMUnsafe.fold {β : Type v} {m : Type v → Type w} [Monad m] (f : βUInt8m β) (as : ByteArray) (i : USize) (stop : USize) (b : β) :
                                            m β
                                            Equations
                                            Instances For
                                              @[implemented_by ByteArray.foldlMUnsafe]
                                              def ByteArray.foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : βUInt8m β) (init : β) (as : ByteArray) (start : optParam Nat 0) (stop : optParam Nat as.size) :
                                              m β

                                              Reference implementation for foldlM

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                def ByteArray.foldlM.loop {β : Type v} {m : Type v → Type w} [Monad m] (f : βUInt8m β) (as : ByteArray) (stop : Nat) (h : stop as.size) (i : Nat) (j : Nat) (b : β) :
                                                m β
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  @[inline]
                                                  def ByteArray.foldl {β : Type v} (f : βUInt8β) (init : β) (as : ByteArray) (start : optParam Nat 0) (stop : optParam Nat as.size) :
                                                  β
                                                  Equations
                                                  Instances For
                                                    Equations
                                                    Instances For
                                                      Equations

                                                      Interpret a ByteArray of size 8 as a little-endian UInt64.

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

                                                        Interpret a ByteArray of size 8 as a big-endian UInt64.

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