chore: add a Repr for Sym2 (#14251)

This matches the approach used by `Multiset`
leanprover-community · Jul 10, 2024 · 529a610 · 529a610
1 parent e242f1e
commit 529a610
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/Mathlib/Data/Sym/Sym2.lean b/Mathlib/Data/Sym/Sym2.lean
@@ -765,4 +765,8 @@ instance [IsEmpty α] : IsEmpty (Sym2 α) :=
 instance [Nontrivial α] : Nontrivial (Sym2 α) :=
   diag_injective.nontrivial
 
+-- 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})"
+
 end Sym2