core / init.data.subtype.instances

@[protected, instance]

def subtype.decidable_eq {α : Type u} {p : α → Prop} [decidable_eq α] :

Equations

subtype.decidable_eq = id (λ (_v : {x // p x}), _v.cases_on (λ (val : α) (property : p val) (w : {x // p x}), w.cases_on (λ (w_val : α) (w_property : p w_val), decidable.by_cases (λ (ᾰ : val = w_val), eq.rec (λ (w_property : p val), decidable.is_true _) ᾰ w_property) (λ (ᾰ : ¬val = w_val), decidable.is_false _))))