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.

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 α