Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.Localization]
public meta def
_aux_Mathlib_RingTheory_DedekindDomain_Instances___delab_app__private_Mathlib_RingTheory_DedekindDomain_Instances_0_termSₚ_1 :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 3
(getExpr✝ >>= fun e✝ =>
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Localization)) (matchFVar✝ `S (matchExpr✝ isType'✝)))
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Algebra.algebraMapSubmonoid))
(matchFVar✝ `R (matchExpr✝ isType'✝)))
pure✝)
(matchFVar✝ `S (matchExpr✝ isType'✝)))
pure✝)
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Ideal.primeCompl))
(matchFVar✝ `R (matchExpr✝ isType'✝)))
pure✝)
(matchFVar✝ `P
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Ideal)) (matchFVar✝ `R (matchExpr✝ isType'✝)))
pure✝)))
pure✝)) >=>
pure✝)
MatchState.empty✝ >>=
fun s✝ => withHeadRefIfTagAppFns✝ `(Sₚ))
