instance instHashableNat : Hashable Nat

Equations

• instHashableNat = { hash := fun (n : Nat) => UInt64.ofNat n }

instance instHashablePos : Hashable String.Pos

Equations

• instHashablePos = { hash := fun (p : String.Pos) => UInt64.ofNat p.byteIdx }

instance instHashableProd {α : Type u_1} {β : Type u_2} [Hashable α] [Hashable β] : Hashable (α × β)

Equations

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

instance instHashableBool : Hashable Bool

Equations

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

instance instHashablePEmpty : Hashable PEmpty

Equations

• instHashablePEmpty = { hash := fun (x : PEmpty) => nomatch x }

instance instHashablePUnit : Hashable PUnit

Equations

• instHashablePUnit = { hash := fun (x : PUnit) => 11 }

instance instHashableOption {α : Type u_1} [Hashable α] : Hashable (Option α)

Equations

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

instance instHashableList {α : Type u_1} [Hashable α] : Hashable (List α)

Equations

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

instance instHashableArray {α : Type u_1} [Hashable α] : Hashable (Array α)

Equations

• instHashableArray = { hash := fun (as : Array α) => Array.foldl (fun (r : UInt64) (a : α) => mixHash r (hash a)) 7 as }

instance instHashableUInt8 : Hashable UInt8

Equations

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

instance instHashableUInt16 : Hashable UInt16

Equations

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

instance instHashableUInt32 : Hashable UInt32

Equations

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

instance instHashableUInt64 : Hashable UInt64

Equations

• instHashableUInt64 = { hash := fun (n : UInt64) => n }

instance instHashableUSize : Hashable USize

Equations

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

instance instHashableByteArray : Hashable ByteArray

Equations

• instHashableByteArray = { hash := fun (as : ByteArray) => ByteArray.foldl (fun (r : UInt64) (a : UInt8) => mixHash r (hash a)) 7 as }

instance instHashableFin {n : Nat} : Hashable (Fin n)

Equations

• instHashableFin = { hash := fun (v : Fin n) => (↑v).toUInt64 }

instance instHashableChar : Hashable Char

Equations

• instHashableChar = { hash := fun (c : Char) => c.val.toUInt64 }

instance instHashableInt : Hashable Int

Equations

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

instance instHashable (P : Prop) : Hashable P

Equations

• instHashable P = { hash := fun (x : P) => 0 }

@[inline]

def hash64 (u : UInt64) : UInt64

An opaque (low-level) hash operation used to implement hashing for pointers.

Equations

• hash64 u = mixHash u 11

class LawfulHashable (α : Type u) [BEq α] [Hashable α] : Prop

The BEq α and Hashable α instances on α are compatible. This means that that a == b implies hash a = hash b.

This is automatic if the BEq instance is lawful.

• hash_eq (a b : α) : (a == b) = true → hash a = hash b

  If a == b, then hash a = hash b.

Instances

• instLawfulHashableOfLawfulBEq

theorem hash_eq {α : Type u_1} [BEq α] [Hashable α] [LawfulHashable α] {a b : α} : (a == b) = true → hash a = hash b

A lawful hash function respects its Boolean equality test.

@[instance 100]

instance instLawfulHashableOfLawfulBEq {α : Type u_1} [BEq α] [Hashable α] [LawfulBEq α] : LawfulHashable α