Lean4
/-- Pretty printer defined by `notation3` command. -/
@[scoped delab✝ app.AlgebraicGeometry.Spec]
public meta def «_aux_Mathlib_AlgebraicGeometry_Scheme___delab_app_SpecOfNotation_termSpec(_)_1» : Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 1
(getExpr✝ >>= fun e✝ =>
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `AlgebraicGeometry.Spec))
(matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `CommRingCat.of)) (matchVar✝ `R)) pure✝) >=>
pure✝)
MatchState.empty✝ >>=
fun s✝ => MatchState.delabVar✝ s✝ `R (some✝ e✝) >>= fun R => withHeadRefIfTagAppFns✝ `(Spec($R)))
