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