chore(data/multiset): move has_repr into its own file to remove data.string.basic import

src/data/finset/default.lean

@@ -8,3 +8,4 @@ import data.finset.pi
 import data.finset.powerset
 import data.finset.sort
 import data.finset.preimage
+import data.finset.repr

src/data/finset/repr.lean

@@ -0,0 +1,13 @@
+/-
+Copyright (c) 2017 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import data.multiset.repr
+import data.finset.sort
+
+/-!
+# Representing a finset as a string
+-/
+
+instance {α : Type*} [has_repr α] : has_repr (finset α) := ⟨λ s, repr s.1⟩

src/data/finset/sort.lean

@@ -211,6 +211,4 @@ by simp only [order_emb_of_card_le, rel_embedding.coe_trans, finset.order_emb_of
 
 end sort_linear_order
 
-instance [has_repr α] : has_repr (finset α) := ⟨λ s, repr s.1⟩
-
 end finset

src/data/list/cycle.lean → src/data/list/cycle/basic.lean

@@ -726,15 +726,6 @@ by { rw [←next_reverse_eq_prev, ←mem_reverse_iff], apply next_mem }
 
 end decidable
 
-/--
-We define a representation of concrete cycles, available when viewing them in a goal state or
-via `#eval`, when over representatble types. For example, the cycle `(2 1 4 3)` will be shown
-as `c[1, 4, 3, 2]`. The representation of the cycle sorts the elements by the string value of the
-underlying element. This representation also supports cycles that can contain duplicates.
--/
-instance [has_repr α] : has_repr (cycle α) :=
-⟨λ s, "c[" ++ string.intercalate ", " ((s.map repr).lists.sort (≤)).head ++ "]"⟩
-
 /-- `chain R s` means that `R` holds between adjacent elements of `s`.
 
 `chain R ([a, b, c] : cycle α) ↔ R a b ∧ R b c ∧ R c a` -/

src/data/list/cycle/default.lean

@@ -0,0 +1 @@
+import data.list.cycle.repr

src/data/list/cycle/repr.lean

@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2021 Yakov Pechersky. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yakov Pechersky
+-/
+import data.list.cycle.basic
+import data.multiset.repr
+
+/-!
+# Representing a cycle as a string
+-/
+
+/--
+We define a representation of concrete cycles, available when viewing them in a goal state or
+via `#eval`, when over representatble types. For example, the cycle `(2 1 4 3)` will be shown
+as `c[1, 4, 3, 2]`. The representation of the cycle sorts the elements by the string value of the
+underlying element. This representation also supports cycles that can contain duplicates.
+-/
+instance {α : Type*} [has_repr α] : has_repr (cycle α) :=
+⟨λ s, "c[" ++ string.intercalate ", " ((s.map repr).lists.sort (≤)).head ++ "]"⟩

src/data/multiset/default.lean

@@ -12,3 +12,4 @@ import data.multiset.pi
 import data.multiset.powerset
 import data.multiset.sections
 import data.multiset.sort
+import data.multiset.repr

src/data/multiset/repr.lean

@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2017 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import data.multiset.sort
+import data.string.basic
+
+/-!
+# Representing a multiset as a string
+-/
+
+instance {α : Type*} [has_repr α] : has_repr (multiset α) :=
+⟨λ s, "{" ++ string.intercalate ", " ((s.map repr).sort (≤)) ++ "}"⟩

src/data/multiset/sort.lean

@@ -5,7 +5,6 @@ Authors: Mario Carneiro
 -/
 import data.list.sort
 import data.multiset.basic
-import data.string.basic
 
 /-!
 # Construct a sorted list from a multiset.
@@ -50,7 +49,4 @@ list.merge_sort_singleton r a
 
 end sort
 
-instance [has_repr α] : has_repr (multiset α) :=
-⟨λ s, "{" ++ string.intercalate ", " ((s.map repr).sort (≤)) ++ "}"⟩
-
 end multiset

src/data/pnat/factors.lean

@@ -24,10 +24,14 @@ the multiplicity of `p` in this factors multiset being the p-adic valuation of `
 /-- The type of multisets of prime numbers.  Unique factorization
  gives an equivalence between this set and ℕ+, as we will formalize
  below. -/
- @[derive [inhabited, has_repr, canonically_ordered_add_monoid, distrib_lattice,
+ @[derive [inhabited, canonically_ordered_add_monoid, distrib_lattice,
   semilattice_sup, order_bot, has_sub, has_ordered_sub]]
 def prime_multiset := multiset nat.primes
 
+-- We could use the `repr` for multisets here, but we want to reduce imports
+instance : has_repr prime_multiset :=
+⟨λ m, repr ((m.map (coe : nat.primes → nat)).sort (≤))⟩
+
 namespace prime_multiset
 
 /-- The multiset consisting of a single prime -/