def StrataDDM.ByteArray.ofNatArray (a : Array Nat) : ByteArray

Equations

• StrataDDM.ByteArray.ofNatArray a = { data := Array.map UInt8.ofNat a }

@[implicit_reducible]

instance StrataDDM.ByteArray.instToExprByteArray_strataDDM : Lean.ToExpr ByteArray

Equations

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

def StrataDDM.ByteArray.asHex (a : ByteArray) : String

Equations

• StrataDDM.ByteArray.asHex a = ByteArray.foldl (fun (s : String) (b : UInt8) => s ++ StrataDDM.ByteArray.byteToHex✝ b) "" a

def StrataDDM.ByteArray.reprPrec (a : ByteArray) (p : Nat) : Std.Format

Equations

• StrataDDM.ByteArray.reprPrec a p = Repr.addAppParen (Std.Format.text "ByteArray.mk " ++ reprArg a.data) p

@[implicit_reducible]

instance StrataDDM.ByteArray.instReprByteArray_strataDDM : Repr ByteArray

Equations

• StrataDDM.ByteArray.instReprByteArray_strataDDM = { reprPrec := StrataDDM.ByteArray.reprPrec }

def StrataDDM.ByteArray.escapedBytes : Std.HashMap UInt8 Char

Equations

• StrataDDM.ByteArray.escapedBytes = Std.HashMap.ofList [(9, 't'), (10, 'n'), (13, 'r'), (34, '\"'), (92, '\\')]

def StrataDDM.ByteArray.escapeBytes (b : ByteArray) : String

Equations

• StrataDDM.ByteArray.escapeBytes b = ByteArray.foldl (fun (s : String) (b : UInt8) => s ++ StrataDDM.ByteArray.escapeBytes.aux✝ b) "b\"" b ++ "\""

@[inline]

def StrataDDM.ByteArray.hexDigitToUInt8 (c : Char) : Option UInt8

Equations

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

def StrataDDM.ByteArray.escapeChars : Std.HashMap Char UInt8

Equations

• StrataDDM.ByteArray.escapeChars = Std.HashMap.ofList (List.map (fun (x : UInt8 × Char) => match x with | (i, c) => (c, i)) StrataDDM.ByteArray.escapedBytes.toList)

partial def StrataDDM.ByteArray.unescapeBytesRawAux (s : String) (i0 : String.Pos.Raw) (a : ByteArray) : Except (String.Pos.Raw × String.Pos.Raw × String) (ByteArray × String.Pos.Raw)

partial def StrataDDM.ByteArray.unescapeBytesAux (s : String) (i0 : s.Pos) (a : ByteArray) : Except (s.Pos × s.Pos × String) (ByteArray × s.Pos)

def StrataDDM.ByteArray.unescapeBytes (s : String) : Except (s.Pos × s.Pos × String) ByteArray

Equations

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