fix(data/equiv/encodable): turn unique.encodable into a def (#10006)

leanprover-community · Oct 28, 2021 · bcaeb57 · bcaeb57
1 parent 9db7270
commit bcaeb57
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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