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