Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.Subtype]
public meta def
«_aux_Mathlib_RingTheory_Finiteness_Basic___delab_app__private_Mathlib_RingTheory_Finiteness_Basic_0_termR≥0_1» :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 2
(getExpr✝ >>= fun e✝ =>
(matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Subtype)) (matchFVar✝ `R (matchExpr✝ isType'✝)))
(matchLambda✝ (matchFVar✝ `R (matchExpr✝ isType'✝))
(fun n✝ =>
matchApp✝¹
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `LE.le))
(matchFVar✝¹ `R (matchExpr✝¹ isType'✝¹)))
pure✝)
(matchApp✝¹
(matchApp✝¹
(matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `OfNat.ofNat))
(matchFVar✝¹ `R (matchExpr✝¹ isType'✝¹)))
(natLitMatcher✝ 0))
pure✝))
(matchExpr✝¹ (· == n✝)))) >=>
pure✝¹)
MatchState.empty✝ >>=
fun s✝ => withHeadRefIfTagAppFns✝ `(R≥0))
