From 1ea56038e3ba62237dd9896754c76b03d2d9ebc1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 2 Jun 2015 10:47:20 -0700
Subject: [PATCH] feat(library/init/quot): add has_decidable_eq definition for
 quotients

---
 library/init/quot.lean | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/library/init/quot.lean b/library/init/quot.lean
index c95ec18b7..355e8acb2 100644
--- a/library/init/quot.lean
+++ b/library/init/quot.lean
@@ -146,3 +146,13 @@ attribute quot.lift₂                [unfold-c 8]
 attribute quot.lift_on₂             [unfold-c 6]
 attribute quot.hrec_on₂             [unfold-c 6]
 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)