English
The Repr instance for polynomials is provided to enable a readable textual representation of polynomials.
Русский
Для многочленов задан инстанс представления (Repr), обеспечивающий читаемость текстового вывода.
LaTeX
$$Repr (Polynomial R)$$
Lean4
protected instance repr [Repr R] [DecidableEq R] : Repr R[X] :=
⟨fun p prec =>
let termPrecAndReprs : List (WithTop ℕ × Lean.Format) :=
List.map
(fun
| 0 => (max_prec, "C " ++ reprArg (coeff p 0))
| 1 => if coeff p 1 = 1 then (⊤, "X") else (70, "C " ++ reprArg (coeff p 1) ++ " * X")
| n =>
if coeff p n = 1 then (80, "X ^ " ++ Nat.repr n)
else (70, "C " ++ reprArg (coeff p n) ++ " * X ^ " ++ Nat.repr n))
(p.support.sort (· ≤ ·))
match termPrecAndReprs with
| [] => "0"
| [(tprec, t)] => if prec ≥ tprec then Lean.Format.paren t else t
| ts =>
-- multiple terms, use `+` precedence
(if prec ≥ 65 then Lean.Format.paren else id)
(Lean.Format.fill (Lean.Format.joinSep (ts.map Prod.snd) (" +" ++ Lean.Format.line)))⟩
