Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.MvPolynomial.X]
public meta def
_aux_Mathlib_AlgebraicGeometry_EllipticCurve_Jacobian_Basic___delab_app__private_Mathlib_AlgebraicGeometry_EllipticCurve_Jacobian_Basic_0_termZ_1_1 :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 4
(getExpr✝ >>= fun e✝ =>
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `MvPolynomial.X)) (matchFVar✝ `R (matchExpr✝ isType'✝)))
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Fin))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(natLitMatcher✝ 3))
pure✝)))
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Fin))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(natLitMatcher✝ 3))
pure✝)))
(natLitMatcher✝ 2))
pure✝) >=>
pure✝)
MatchState.empty✝ >>=
fun s✝ => withHeadRefIfTagAppFns✝ `(Z))
