Lean4
/-- Pretty printer defined by `notation3` command. -/
@[scoped delab✝ app.WithTop.some]
public meta def «_aux_Mathlib_Analysis_Calculus_ContDiff_FTaylorSeries___delab_app_ContDiff_term∞_1» : Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 2
(getExpr✝ >>= fun e✝ =>
(matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `WithTop.some)) (matchExpr✝ (Expr.isConstOf✝ · `ENat)))
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Top.top)) (matchExpr✝ (Expr.isConstOf✝ · `ENat)))
pure✝) >=>
pure✝)
MatchState.empty✝ >>=
fun s✝ => withHeadRefIfTagAppFns✝ `(∞))
