refactor(logic/encodable/small): migrate to countable (#15557)

leanprover-community · Jul 20, 2022 · 6fed037 · 6fed037
1 parent 0c79da0
commit 6fed037
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/src/logic/encodable/small.lean → src/data/countable/small.lean b/src/logic/encodable/small.lean → src/data/countable/small.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import logic.encodable.basic
+import data.countable.basic
 import logic.small
 
 /-!
@@ -15,5 +15,5 @@ That is, any encodable type is equivalent to a type in any universe.
 universes w v
 
 @[priority 100]
-instance small_of_encodable (α : Type v) [encodable α] : small.{w} α :=
-small_of_injective encodable.encode_injective
+instance small_of_countable (α : Type v) [countable α] : small.{w} α :=
+let ⟨f, hf⟩ := exists_injective_nat α in small_of_injective hf
diff --git a/src/logic/small.lean b/src/logic/small.lean
@@ -94,7 +94,7 @@ begin
 end
 
 /-!
-We don't define `small_of_fintype` or `small_of_encodable` in this file,
+We don't define `small_of_fintype` or `small_of_countable` in this file,
 to keep imports to `logic` to a minimum.
 -/