From 62619d538020b455abc5bc0c23bf4e01a2b9fb8d Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 29 Jun 2024 02:09:22 +0100 Subject: [PATCH 1/2] chore: add a `Repr` for `Sym2` This matches the approach used by `Multiset` --- Mathlib/Data/Sym/Sym2.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/Data/Sym/Sym2.lean b/Mathlib/Data/Sym/Sym2.lean index effc02772a5cc9..85a9ebce920ac3 100644 --- a/Mathlib/Data/Sym/Sym2.lean +++ b/Mathlib/Data/Sym/Sym2.lean @@ -764,4 +764,8 @@ instance [IsEmpty α] : IsEmpty (Sym2 α) := instance [Nontrivial α] : Nontrivial (Sym2 α) := diag_injective.nontrivial +-- TODO: use a sort order if available, gh-18166 +unsafe instance [Repr α] : Repr (Sym2 α) where + reprPrec s _ := f!"s({repr s.unquot.1}, {repr s.unquot.2})" + end Sym2 From 57a51a7981b357ee173ca45db807c8d023c1296d Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 3 Jul 2024 01:25:21 +0100 Subject: [PATCH 2/2] Update Mathlib/Data/Sym/Sym2.lean --- Mathlib/Data/Sym/Sym2.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/Sym/Sym2.lean b/Mathlib/Data/Sym/Sym2.lean index 85a9ebce920ac3..e4bc2fcaaadb7a 100644 --- a/Mathlib/Data/Sym/Sym2.lean +++ b/Mathlib/Data/Sym/Sym2.lean @@ -764,7 +764,7 @@ instance [IsEmpty α] : IsEmpty (Sym2 α) := instance [Nontrivial α] : Nontrivial (Sym2 α) := diag_injective.nontrivial --- TODO: use a sort order if available, gh-18166 +-- TODO: use a sort order if available, https://github.com/leanprover-community/mathlib/issues/18166 unsafe instance [Repr α] : Repr (Sym2 α) where reprPrec s _ := f!"s({repr s.unquot.1}, {repr s.unquot.2})"