Quotient types #

These are ported from the Lean 3 standard library file init/data/quot.lean.

inductive EqvGen {α : Type u} (r : ααProp) :

EqvGen r is the equivalence relation generated by r.

Instances For
    theorem EqvGen.is_equivalence {α : Type u} (r : ααProp) :
    def EqvGen.Setoid {α : Type u} (r : ααProp) :

    EqvGen.Setoid r is the setoid generated by a relation r.

    The motivation for this definition is that Quot r behaves like Quotient (EqvGen.Setoid r), see for example Quot.exact and Quot.EqvGen_sound.

    Instances For
      theorem Quot.exact {α : Type u} (r : ααProp) {a : α} {b : α} (H : r a = r b) :
      EqvGen r a b
      theorem Quot.EqvGen_sound {α : Type u} {r : ααProp} {a : α} {b : α} (H : EqvGen r a b) : r a = r b
      instance Quotient.decidableEq {α : Sort u} {s : Setoid α} [d : (a b : α) → Decidable (a b)] :