Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.Set.range]
public meta def
«_aux_Mathlib_Algebra_Polynomial_CoeffMem___delab_app__private_Mathlib_Algebra_Polynomial_CoeffMem_0_Polynomial_termCoeffs(_)_1» :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 3
(getExpr✝ >>= fun e✝ =>
(matchApp✝
(matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Set.range)) pure✝)
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(matchApp✝ (matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Polynomial.coeff)) pure✝) pure✝)
(matchVar✝ `p)) >=>
pure✝)
MatchState.empty✝ >>=
fun s✝ => MatchState.delabVar✝ s✝ `p (some✝ e✝) >>= fun p => withHeadRefIfTagAppFns✝ `(coeffs($p)))
