_aux_Mathlib_Combinatorics_Additive_DoublingConst___delab_app_Combinatorics_Additive_termσₘ[_,_]_1

Lean4

/-- Pretty printer defined by `notation3` command. -/
@[scoped delab✝ app.Finset.mulConst]
public meta def «_aux_Mathlib_Combinatorics_Additive_DoublingConst___delab_app_Combinatorics_Additive_termσₘ[_,_]_1» :
    Delab✝ :=
  whenPPOption✝ getPPNotation✝ <|
    whenNotPPOption✝ getPPExplicit✝ <|
      withOverApp✝ 5
        (getExpr✝ >>= fun e✝ =>
          (matchApp✝
                  (matchApp✝
                    (matchApp✝ (matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Finset.mulConst)) pure✝) pure✝)
                      pure✝)
                    (matchVar✝ `A))
                  (matchVar✝ `B) >=>
                pure✝)
              MatchState.empty✝ >>=
            fun s✝ =>
            MatchState.delabVar✝ s✝ `A (some✝ e✝) >>= fun A =>
              MatchState.delabVar✝ s✝ `B (some✝ e✝) >>= fun B => withHeadRefIfTagAppFns✝ `(σₘ[$A, $B]))

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