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