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
instance instHashableFin {n : Nat} :
Equations
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