Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.Max.max]
public meta def
«_aux_Mathlib_Algebra_Polynomial_CoeffMem___delab_app__private_Mathlib_Algebra_Polynomial_CoeffMem_0_Polynomial_termSpanCoeffs(_)_1» :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 4
(getExpr✝ >>= fun e✝ =>
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Max.max))
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Submodule))
(matchFVar✝ `R (matchExpr✝ isType'✝)))
pure✝)
pure✝)
pure✝)
pure✝))
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Submodule))
(matchFVar✝ `R (matchExpr✝ isType'✝)))
pure✝)
pure✝)
pure✝)
pure✝))
(natLitMatcher✝ 1))
pure✝))
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Submodule.span))
(matchFVar✝ `R (matchExpr✝ isType'✝)))
pure✝)
pure✝)
pure✝)
pure✝)
(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✝ `(spanCoeffs($p)))
