Hash Types

@[reducible, inline]

abbrev ByteVector (n : Nat) : Type

Equations

• ByteVector = Vector UInt8

def ByteVector.toInt {sz : Nat} (vc : ByteVector sz) : Int

Equations

• vc.toInt = Vector.foldl (fun (acc : Int) (nb : UInt8) => acc + Int.ofNat nb.toNat) 0 vc

@[reducible, inline]

abbrev Word28 : Type

Equations

• Word28 = ByteVector 28

@[reducible, inline]

abbrev Word32 : Type

Equations

• Word32 = ByteVector 32

@[reducible, inline]

abbrev Word64 : Type

Equations

• Word64 = ByteVector 64

@[reducible, inline]

abbrev Hash_28 : Type

Equations

• Hash_28 = ByteVector 28

@[reducible, inline]

abbrev Hash_28.zero : Hash_28

Equations

• Hash_28.zero = Vector.replicate 28 0

@[reducible, inline]

abbrev Hash_32 : Type

Equations

• Hash_32 = ByteVector 32

@[reducible, inline]

abbrev Hash_32.zero : Hash_32

Equations

• Hash_32.zero = Vector.replicate 32 0

@[reducible, inline]

abbrev Hash_64 : Type

Equations

• Hash_64 = Nat

@[reducible, inline]

abbrev Hash_64.zero : Hash_64

Equations

• Hash_64.zero = 0

Time

@[reducible, inline]

abbrev PosixTime : Type

Equations

• PosixTime = Nat

Operators Id

@[reducible, inline]

abbrev OperatorId : Type

Equations

• OperatorId = Nat