Documentation

Init.Data.Hashable

instance instHashableNat:

Equations

instHashableNat = { hash := fun n => UInt64.ofNat n }

instance instHashablePos:

Hashable String.Pos

Equations

instHashablePos = { hash := fun p => UInt64.ofNat p.byteIdx }

instance instHashableProd {α : Type u_1} {β : Type u_2} [inst : Hashable α] [inst : Hashable β] :

Hashable (α × β)

Equations

instHashableProd = { hash := fun x => match x with | (a, b) => mixHash (hash a) (hash b) }

instance instHashableBool:

Equations

instHashableBool = { hash := fun x => match x with | true => 11 | false => 13 }

instance instHashableOption {α : Type u_1} [inst : Hashable α] :

Hashable (Option α)

Equations

instHashableOption = { hash := fun x => match x with | none => 11 | some a => mixHash (hash a) 13 }

instance instHashableList {α : Type u_1} [inst : Hashable α] :

Hashable (List α)

Equations

instHashableList = { hash := fun as => List.foldl (fun r a => mixHash r (hash a)) 7 as }

instance instHashableArray {α : Type u_1} [inst : Hashable α] :

Hashable (Array α)

Equations

instHashableArray = { hash := fun as => Array.foldl (fun r a => mixHash r (hash a)) 7 as 0 (Array.size as) }

instance instHashableUInt8:

Equations

instHashableUInt8 = { hash := fun n => UInt8.toUInt64 n }

instance instHashableUInt16:

Hashable UInt16

Equations

instHashableUInt16 = { hash := fun n => UInt16.toUInt64 n }

instance instHashableUInt32:

Hashable UInt32

Equations

instHashableUInt32 = { hash := fun n => UInt32.toUInt64 n }

instance instHashableUInt64:

Hashable UInt64

Equations

instHashableUInt64 = { hash := fun n => n }

instance instHashableUSize:

Equations

instHashableUSize = { hash := fun n => USize.toUInt64 n }

instance instHashableFin {n : Nat} :

Hashable (Fin n)

Equations

instHashableFin = { hash := fun v => Nat.toUInt64 v.val }

instance instHashableInt:

Equations

instHashableInt = { hash := fun x => match x with | Int.ofNat n => UInt64.ofNat (2 * n) | Int.negSucc n => UInt64.ofNat (2 * n + 1) }

instance instHashable (P : Prop) :

Equations

instHashable P = { hash := fun x => 0 }