Init.Data.Hashable

source

instance instHashableNat :

Hashable Nat

Equations

source

instance instHashablePos :

Hashable String.Pos

Equations

source

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

Hashable (α × β)

Equations

source

instance instHashableBool :

Hashable Bool

Equations

source

instance instHashablePEmpty :

Hashable PEmpty

Equations

source

instance instHashablePUnit :

Hashable PUnit

Equations

source

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

Hashable (Option α)

Equations

source

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

Hashable (List α)

Equations

source

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

Hashable (Array α)

Equations

source

instance instHashableUInt8 :

Hashable UInt8

Equations

source

instance instHashableUInt16 :

Hashable UInt16

Equations

source

instance instHashableUInt32 :

Hashable UInt32

Equations

source

instance instHashableUInt64 :

Hashable UInt64

Equations

source

instance instHashableUSize :

Hashable USize

Equations

source

instance instHashableFin {n : Nat} :

Hashable (Fin n)

Equations

source

instance instHashableChar :

Hashable Char

Equations

source

instance instHashableInt :

Hashable Int

Equations

source

instance instHashable (P : Prop) :

Hashable P

Equations

source

@[inline]

def hash64 (u : UInt64) :

UInt64

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

Equations

Instances For

source

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

source

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.

source

@[instance 100]

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

LawfulHashable α