def Cryptlib.Util.newhex.byteToHex (b : UInt8) : String

Equations

• Cryptlib.Util.newhex.byteToHex b = toString (hexDigitRepr (b.toNat / 16)) ++ toString (hexDigitRepr (b.toNat % 16))

def Cryptlib.Util.newhex.byteArrayToHex (blob : ByteArray) : String

Equations

• Cryptlib.Util.newhex.byteArrayToHex blob = ByteArray.foldl (fun (acc : String) (b : UInt8) => acc ++ Cryptlib.Util.newhex.byteToHex b) "" blob

@[instance_reducible]

instance Cryptlib.Util.newhex.instReprByteArray_cryptlib : Repr ByteArray

Equations

• Cryptlib.Util.newhex.instReprByteArray_cryptlib = { reprPrec := fun (a : ByteArray) (x : ℕ) => Std.Format.text (Cryptlib.Util.newhex.byteArrayToHex a) }

@[instance_reducible]

instance Cryptlib.Util.newhex.instToStringByteArray_cryptlib : ToString ByteArray

Equations

• Cryptlib.Util.newhex.instToStringByteArray_cryptlib = { toString := fun (x : ByteArray) => Cryptlib.Util.newhex.byteArrayToHex x }

def Cryptlib.Util.newhex.hexCharToDigit (c : Char) : Option UInt8

Equations

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

def Cryptlib.Util.newhex.hexToByte (high low : Char) : Option UInt8

Equations

• Cryptlib.Util.newhex.hexToByte high low = match Cryptlib.Util.newhex.hexCharToDigit high, Cryptlib.Util.newhex.hexCharToDigit low with | some h, some l => some (h <<< 4 ||| l) | x, x_1 => none

def Cryptlib.Util.newhex.hexStringToByteArrayAux : List Char → List UInt8 → Option (List UInt8)

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Util.newhex.hexStringToByteArrayAux [] x✝ = some x✝.reverse
• Cryptlib.Util.newhex.hexStringToByteArrayAux [head] x✝ = none

def Cryptlib.Util.newhex.hexStringToByteArray (s : String) : Option ByteArray

Equations

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

def Cryptlib.Util.newhex.falliableHexStringToByteArray (s : String) : ByteArray

Equations

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