From 3fcbff61e79ba30dedc20928e789c1e202220177 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Thu, 20 Apr 2023 08:51:52 +0000
Subject: [PATCH] add test cases

---
 Mathlib/Data/Polynomial/Basic.lean | 22 ++++++++++++++++++----
 1 file changed, 18 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Data/Polynomial/Basic.lean b/Mathlib/Data/Polynomial/Basic.lean
index d1fc2c2f9173a..4df1134cd5289 100644
--- a/Mathlib/Data/Polynomial/Basic.lean
+++ b/Mathlib/Data/Polynomial/Basic.lean
@@ -1221,10 +1221,10 @@ section repr
 variable [Semiring R]
 
 protected instance repr [Repr R] [DecidableEq R] : Repr R[X] :=
-  ⟨fun p prec =>
+  ⟨fun p _ =>
     if p.support = ∅ then "0"
     else
-      Repr.addAppParen
+      Lean.Format.paren
         (Lean.Format.fill
           (Lean.Format.joinSep
             (List.map
@@ -1235,10 +1235,24 @@ protected instance repr [Repr R] [DecidableEq R] : Repr R[X] :=
                   if coeff p n = 1 then "X ^ " ++ Nat.repr n
                   else "C " ++ reprArg (coeff p n) ++ " * X ^ " ++ Nat.repr n)
               (p.support.sort (· ≤ ·)))
-            (" +" ++ Lean.Format.line)))
-        prec⟩
+            (" +" ++ Lean.Format.line)))⟩
 #align polynomial.has_repr Polynomial.repr
 
+example : reprStr
+    (⟨⟨{}, Pi.single 0 0,
+      by intro; simp [Pi.single, Function.update_apply]⟩⟩ : ℕ[X]) =
+    "0" := by native_decide
+
+example : reprStr
+    (⟨⟨{1}, Pi.single 1 37,
+      by intro; simp [Pi.single, Function.update_apply]⟩⟩ : ℕ[X]) =
+    "(C 37 * X)" := by native_decide
+
+example : reprStr
+    (⟨⟨{0, 2}, Pi.single 0 57 + Pi.single 2 22,
+      by intro; simp [Pi.single, Function.update_apply]; tauto⟩⟩ : ℕ[X]) =
+    "(C 57 + C 22 * X ^ 2)" := by native_decide
+
 end repr
 
 end Polynomial