_aux_Mathlib_Data_Quot___delab_app_Quotient_term⟦_⟧_1

Lean4

/-- Pretty printer defined by `notation3` command. -/
@[delab✝ app.Quotient.mk]
public meta def «_aux_Mathlib_Data_Quot___delab_app_Quotient_term⟦_⟧_1» : Delab✝ :=
  whenPPOption✝ getPPNotation✝ <|
    whenNotPPOption✝ getPPExplicit✝ <|
      withOverApp✝ 3
        (getExpr✝ >>= fun e✝ =>
          (matchApp✝ (matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Quotient.mk)) pure✝) pure✝)
                  (matchVar✝ `a) >=>
                pure✝)
              MatchState.empty✝ >>=
            fun s✝ => MatchState.delabVar✝ s✝ `a (some✝ e✝) >>= fun a => withHeadRefIfTagAppFns✝ `(⟦$a⟧))

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