Documentation

Std.Classes.BEq

Boolean equality #

class PartialEquivBEq (α : Type u_1) [inst : BEq α] :
  • Symmetry for BEq. If a == b then b == a.

    symm : ∀ {a b : α}, (a == b) = true(b == a) = true
  • Transitivity for BEq. If a == b and b == c then a == c.

    trans : ∀ {a b c : α}, (a == b) = true(b == c) = true(a == c) = true

PartialEquivBEq α says that the BEq implementation is a partial equivalence relation, that is:

  • it is symmetric: a == b → b == a→ b == a
  • it is transitive: a == b → b == c → a == c→ b == c → a == c→ a == c.
Instances
    @[simp]
    theorem beq_eq_false_iff_ne {α : Type u_1} [inst : BEq α] [inst : LawfulBEq α] (a : α) (b : α) :
    (a == b) = false a b