diff --git a/src/data/finset/sort.lean b/src/data/finset/sort.lean index 1ced1d74ff4f2..c293a1d344bf9 100644 --- a/src/data/finset/sort.lean +++ b/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 diff --git a/src/data/list/cycle.lean b/src/data/list/cycle.lean index 60dc82c3a7e7b..8cfba07a9c6a6 100644 --- a/src/data/list/cycle.lean +++ b/src/data/list/cycle.lean @@ -17,8 +17,8 @@ Based on this, we define the quotient of lists by the rotation relation, called We also 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. +as `c[2, 1, 4, 3]`. Two equal cycles may be printed differently if their internal representation +is different. -/ @@ -728,12 +728,12 @@ 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. +via `#eval`, when over representable types. For example, the cycle `(2 1 4 3)` will be shown +as `c[2, 1, 4, 3]`. Two equal cycles may be printed differently if their internal representation +is different. -/ -instance [has_repr α] : has_repr (cycle α) := -⟨λ s, "c[" ++ string.intercalate ", " ((s.map repr).lists.sort (≤)).head ++ "]"⟩ +meta instance [has_repr α] : has_repr (cycle α) := +⟨λ s, "c[" ++ string.intercalate ", " ((s.map repr).lists.unquot).head ++ "]"⟩ /-- `chain R s` means that `R` holds between adjacent elements of `s`. diff --git a/src/data/multiset/sort.lean b/src/data/multiset/sort.lean index df8ecbe0d9e4b..648d975765165 100644 --- a/src/data/multiset/sort.lean +++ b/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,8 @@ list.merge_sort_singleton r a end sort -instance [has_repr α] : has_repr (multiset α) := -⟨λ s, "{" ++ string.intercalate ", " ((s.map repr).sort (≤)) ++ "}"⟩ +-- TODO: use a sort order if available, gh-18166 +meta instance [has_repr α] : has_repr (multiset α) := +⟨λ s, "{" ++ string.intercalate ", " (s.unquot.map repr) ++ "}"⟩ end multiset diff --git a/src/data/pnat/factors.lean b/src/data/pnat/factors.lean index 40fd6f53fc58c..f49517117765b 100644 --- a/src/data/pnat/factors.lean +++ b/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 +-- `@[derive]` doesn't work for `meta` instances +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) diff --git a/src/group_theory/perm/cycle/concrete.lean b/src/group_theory/perm/cycle/concrete.lean index 03a7eb22a2180..d52b8721d9ebc 100644 --- a/src/group_theory/perm/cycle/concrete.lean +++ b/src/group_theory/perm/cycle/concrete.lean @@ -537,7 +537,7 @@ def iso_cycle' : {f : perm α // is_cycle f} ≃ {s : cycle α // s.nodup ∧ s. notation `c[` l:(foldr `, ` (h t, list.cons h t) list.nil `]`) := cycle.form_perm ↑l (cycle.nodup_coe_iff.mpr dec_trivial) -instance repr_perm [has_repr α] : has_repr (perm α) := +meta instance repr_perm [has_repr α] : has_repr (perm α) := ⟨λ f, repr (multiset.pmap (λ (g : perm α) (hg : g.is_cycle), iso_cycle ⟨g, hg⟩) -- to_cycle is faster? (perm.cycle_factors_finset f).val diff --git a/test/cycle.lean b/test/cycle.lean index 90b5222aa9fb7..bc3424ef5b4bb 100644 --- a/test/cycle.lean +++ b/test/cycle.lean @@ -1,5 +1,5 @@ import data.list.cycle run_cmd guard ("c[1, 4, 3, 2]" = repr (↑[1, 4, 3, 2] : cycle ℕ)) -run_cmd guard ("c[1, 4, 3, 2]" = repr (↑[2, 1, 4, 3] : cycle ℕ)) -run_cmd guard ("c[-1, 2, 1, 4]" = repr (↑[(2 : ℤ), 1, 4, -1] : cycle ℤ)) +run_cmd guard ("c[2, 1, 4, 3]" = repr (↑[2, 1, 4, 3] : cycle ℕ)) +run_cmd guard ("c[2, 1, 4, -1]" = repr (↑[(2 : ℤ), 1, 4, -1] : cycle ℤ))