mathlib3 documentation

core / init.data.subtype.instances

@[protected, instance]
def subtype.decidable_eq {α : Type u} {p : α Prop} [decidable_eq α] :
decidable_eq {x // p x}
Equations