_aux_Mathlib_Data_Quot___delab_app__private_Mathlib_Data_Quot_0_Quot_term⟦_⟧_1

Lean4

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

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