From bcaeb57a20248edffa90bca554d9e7e9439614df Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Thu, 28 Oct 2021 04:50:37 +0000
Subject: [PATCH] fix(data/equiv/encodable): turn `unique.encodable` into a
 `def` (#10006)

---
 src/data/equiv/encodable/basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/data/equiv/encodable/basic.lean b/src/data/equiv/encodable/basic.lean
index cbb813a0cba60..aca7245fa3b84 100644
--- a/src/data/equiv/encodable/basic.lean
+++ b/src/data/equiv/encodable/basic.lean
@@ -161,8 +161,8 @@ def equiv_range_encode (α : Type*) [encodable α] : α ≃ set.range (@encode 
     rw [encode_injective.eq_iff, ← option.some_inj, option.some_get, ← hx, encodek₂],
   end }
 
-/-- A type with unique element is encodable. -/
-@[priority 100] instance _root_.unique.encodable [unique α] : encodable α :=
+/-- A type with unique element is encodable. This is not an instance to avoid diamonds. -/
+def _root_.unique.encodable [unique α] : encodable α :=
 ⟨λ _, 0, λ _, some (default α), unique.forall_iff.2 rfl⟩
 
 section sum