_aux_Mathlib_Data_Sym_Sym2___delab_app_termS(_,_)_1

Lean4
/-- Pretty printer defined by `notation3` command. -/
@[delab✝ app.Sym2.mk]
public meta def «_aux_Mathlib_Data_Sym_Sym2___delab_app_termS(_,_)_1» : Delab✝ :=
  whenPPOption✝ getPPNotation✝ <|
    whenNotPPOption✝ getPPExplicit✝ <|
      withOverApp✝ 2
        (getExpr✝ >>= fun e✝ =>
          (matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Sym2.mk)) pure✝)
                  (matchApp✝
                    (matchApp✝ (matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Prod.mk)) pure✝) pure✝)
                      (matchVar✝ `x))
                    (matchVar✝ `y)) >=>
                pure✝)
              MatchState.empty✝ >>=
            fun s✝ =>
            MatchState.delabVar✝ s✝ `x (some✝ e✝) >>= fun x =>
              MatchState.delabVar✝ s✝ `y (some✝ e✝) >>= fun y => withHeadRefIfTagAppFns✝ `(s($x, $y)))
Похожие утверждения