class Cryptlib.Util.Serial.SerialUInt32 (X : Type) : Type

• words : Nat
• toUInt32Words : X → Array UInt32
• fromUInt32Words : Subarray UInt32 → X

@[instance_reducible]

instance Cryptlib.Util.Serial.instSerialUInt32UInt32 : SerialUInt32 UInt32

Equations

• Cryptlib.Util.Serial.instSerialUInt32UInt32 = { words := 1, toUInt32Words := fun (x : UInt32) => #[x], fromUInt32Words := fun (x : Subarray UInt32) => x[0]! }

class Cryptlib.Util.Serial.SerialWords (Word X : Type) : Type

• words : Nat
• toWords : X → Array Word
• fromWords : Subarray Word → X

@[instance_reducible]

instance Cryptlib.Util.Serial.instSerialWordsUInt32 : SerialWords UInt32 UInt32

Equations

• Cryptlib.Util.Serial.instSerialWordsUInt32 = { words := 1, toWords := fun (x : UInt32) => #[x], fromWords := fun (x : Subarray UInt32) => x[0]! }

@[instance_reducible]

instance Cryptlib.Util.Serial.instSerialWordsUInt64 : SerialWords UInt64 UInt64

Equations

• Cryptlib.Util.Serial.instSerialWordsUInt64 = { words := 1, toWords := fun (x : UInt64) => #[x], fromWords := fun (x : Subarray UInt64) => x[0]! }