[Merged by Bors] - chore(data/multiset/sort): make multiset repr a meta instance

src/data/finset/sort.lean

@@ -211,6 +211,6 @@ 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⟩
+meta instance [has_repr α] : has_repr (finset α) := ⟨λ s, repr s.1⟩
 
 end finset

src/data/list/cycle.lean

@@ -732,7 +732,7 @@ via `#eval`, when over representatble types. For example, the cycle `(2 1 4 3)`
 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 α) :=
+meta 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`.

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,9 @@ list.merge_sort_singleton r a
 
 end sort
 
-instance [has_repr α] : has_repr (multiset α) :=
-⟨λ s, "{" ++ string.intercalate ", " ((s.map repr).sort (≤)) ++ "}"⟩
+meta instance [has_repr α] : has_repr (multiset α) :=
+⟨λ s, "{" ++ string.intercalate ", "
+    (@multiset.sort string (λ s₁ s₂, s₁.to_list ≤ s₂.to_list)
+      undefined undefined undefined undefined (s.map repr) ) ++ "}"⟩
 
 end multiset

src/data/pnat/factors.lean

@@ -24,12 +24,15 @@ 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
 
 namespace prime_multiset
 
+meta instance : has_repr prime_multiset :=
+by delta prime_multiset; apply_instance
+
 /-- The multiset consisting of a single prime -/
 def of_prime (p : nat.primes) : prime_multiset := ({p} : multiset nat.primes)