Documentation

Init.Data.Hashable

Equations
Equations
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) }
Equations
instance instHashableOption {α : Type u_1} [Hashable α] :
Equations
  • instHashableOption = { hash := fun (x : Option α) => match x with | none => 11 | some a => mixHash (hash a) 13 }
instance instHashableList {α : Type u_1} [Hashable α] :
Equations
instance instHashableArray {α : Type u_1} [Hashable α] :
Equations
Equations
Equations
Equations
Equations
Equations
instance instHashableFin {n : Nat} :
Equations
  • instHashableFin = { hash := fun (v : Fin n) => (↑v).toUInt64 }
Equations
instance instHashable (P : Prop) :
Equations
@[inline]
def hash64 (u : UInt64) :

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

Equations
Instances For
    class LawfulHashable (α : Type u) [BEq α] [Hashable α] :

    LawfulHashable α says that the BEq α and Hashable α instances on α are compatible, i.e., that a == b implies hash a = hash b. This is automatic if the BEq instance is lawful.

    • hash_eq : ∀ (a b : α), (a == b) = truehash a = hash b

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

    Instances
      theorem LawfulHashable.hash_eq {α : Type u} :
      ∀ {inst : BEq α} {inst_1 : Hashable α} [self : LawfulHashable α] (a b : α), (a == b) = truehash a = hash b

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

      theorem hash_eq {α : Type u_1} [BEq α] [Hashable α] [LawfulHashable α] {a : α} {b : α} :
      (a == b) = truehash a = hash b
      @[instance 100]
      Equations
      • instLawfulHashableOfLawfulBEq = { hash_eq := }