Lean4
/-- Pretty printer defined by `notation3` command. -/
@[scoped delab✝ app.modelWithCornersSelf]
public meta def _aux_Mathlib_Geometry_Manifold_Instances_Real___delab_app_Manifold_term𝓡__1 : Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 5
(getExpr✝ >>= fun e✝ =>
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `modelWithCornersSelf))
(matchExpr✝ (Expr.isConstOf✝ · `Real)))
pure✝)
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `EuclideanSpace))
(matchExpr✝ (Expr.isConstOf✝ · `Real)))
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Fin)) (matchVar✝ `n))))
pure✝)
pure✝ >=>
pure✝)
MatchState.empty✝ >>=
fun s✝ => MatchState.delabVar✝ s✝ `n (some✝ e✝) >>= fun n => withHeadRefIfTagAppFns✝ `(𝓡 $n))
