_aux_Mathlib_RingTheory_DedekindDomain_Instances___delab_app__private_Mathlib_RingTheory_DedekindDomain_Instances_0_termRₚ_1

Lean4

/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.Localization.AtPrime]
public meta def
  _aux_Mathlib_RingTheory_DedekindDomain_Instances___delab_app__private_Mathlib_RingTheory_DedekindDomain_Instances_0_termRₚ_1 :
    Delab✝ :=
  whenPPOption✝ getPPNotation✝ <|
    whenNotPPOption✝ getPPExplicit✝ <|
      withOverApp✝ 4
        (getExpr✝ >>= fun e✝ =>
          (matchApp✝
                  (matchApp✝
                    (matchApp✝
                      (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Localization.AtPrime))
                        (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✝ `(Rₚ))

Похожие утверждения