Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.CommRingCat.of]
public meta def
«_aux_Mathlib_AlgebraicGeometry_AffineSpace___delab_app__private_Mathlib_AlgebraicGeometry_AffineSpace_0_AlgebraicGeometry_termℤ[_].{_,_}_1» :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 2
(getExpr✝ >>= fun e✝ =>
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `CommRingCat.of))
(matchApp✝
(matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `MvPolynomial)) (matchVar✝ `n))
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `ULift)) (matchExpr✝ (Expr.isConstOf✝ · `Int))))
pure✝))
pure✝ >=>
pure✝)
MatchState.empty✝ >>=
fun s✝ =>
MatchState.delabVar✝ s✝ `u (some✝ e✝) >>= fun u =>
MatchState.delabVar✝ s✝ `n (some✝ e✝) >>= fun n =>
MatchState.delabVar✝ s✝ `v (some✝ e✝) >>= fun v => withHeadRefIfTagAppFns✝ `(ℤ[$n].{$u,$v}))
