Mathlib Map

Structures · Lean core

LawfulBEq

A Boolean equality test coincides with propositional equality. In other words: * a == b implies a = b. * a == a is true.

Defined in
Init.Core
Shape
One type argument · adds eq_of_beq
Open in Mathlib docs

Extends1

Extended by0

Nothing extends this class yet.

Concrete types that are instances31

  • Int
  • Nat
  • Bool
  • Char
  • String
  • Vector
  • Lean.Name
  • Float.Model.UnpackedFloat.Sign
  • Std.ExtTreeMap
  • Std.Http.Header.Name
  • Std.ExtHashMap
  • Lean.Grind.AC.Seq
  • Std.ExtDTreeMap
  • Std.ExtTreeSet
  • Std.ExtDHashMap
  • Std.ExtHashSet
  • Lean.Grind.CommRing.Mon
  • Batteries.AssocList
  • Lean.Grind.CommRing.Power
  • Lean.Grind.CommRing.Poly
  • Int.Internal.Linear.Poly
  • Lean.Grind.Linarith.Poly
  • Nat.Internal.Linear.PolyCnstr
  • Lean.Grind.IntInterval
  • Subtype
  • Prod
  • Lex
  • Colex
  • List
  • Option
  • Array

How is a type an instance?

Loading the hierarchy index…

Assumed by56

Ancestors1