Documentation

Init.Data.Hashable

Equations
Equations
instance instHashableProd {α : Type u_1} {β : Type u_2} [inst : Hashable α] [inst : Hashable β] :
Hashable (α × β)
Equations
  • instHashableProd = { hash := fun _fun_discr => match _fun_discr with | (a, b) => mixHash (hash a) (hash b) }
Equations
instance instHashableOption {α : Type u_1} [inst : Hashable α] :
Equations
  • instHashableOption = { hash := fun _fun_discr => match _fun_discr with | none => 11 | some a => mixHash (hash a) 13 }
instance instHashableList {α : Type u_1} [inst : Hashable α] :
Equations
instance instHashableArray {α : Type u_1} [inst : Hashable α] :
Equations
Equations
Equations
Equations
Equations
Equations
instance instHashableFin {n : Nat} :
Equations
Equations
instance instHashable (P : Prop) :
Equations