michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/init/quot): add has_decidable_eq definition for quotients

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-02 10:47:20 -07:00
parent cfb102cbd1
commit 1ea56038e3
1 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
library/init/quot.lean
View file

@ -146,3 +146,13 @@ attribute quot.lift₂ [unfold-c 8]
attribute quot.lift_on₂ [unfold-c 6] attribute quot.lift_on₂ [unfold-c 6]
attribute quot.hrec_on₂ [unfold-c 6] attribute quot.hrec_on₂ [unfold-c 6]
attribute quot.rec_on_subsingleton₂ [unfold-c 7] attribute quot.rec_on_subsingleton₂ [unfold-c 7]
open decidable
definition quot.has_decidable_eq [instance] {A : Type} {s : setoid A} [decR : ∀ a b : A, decidable (a ≈ b)] : decidable_eq (quot s) :=
λ q₁ q₂ : quot s,
quot.rec_on_subsingleton₂ q₁ q₂
(λ a₁ a₂,
match decR a₁ a₂ with
| inl h₁ := inl (quot.sound h₁)
| inr h₂ := inr (λ h, absurd (quot.exact h) h₂)
end)