_aux_Mathlib_AlgebraicTopology_SimplicialSet_StdSimplex___delab_app_Simplicial_termΔ[_]_1

Lean4
/-- Pretty printer defined by `notation3` command. -/
@[scoped delab✝ app.CategoryTheory.Functor.obj]
public meta def «_aux_Mathlib_AlgebraicTopology_SimplicialSet_StdSimplex___delab_app_Simplicial_termΔ[_]_1» : Delab✝ :=
  whenPPOption✝ getPPNotation✝ <|
    whenNotPPOption✝ getPPExplicit✝ <|
      withOverApp✝ 6
        (getExpr✝ >>= fun e✝ =>
          (matchApp✝
                  (matchApp✝
                    (matchApp✝
                      (matchApp✝
                        (matchApp✝
                          (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `CategoryTheory.Functor.obj))
                            (matchExpr✝ (Expr.isConstOf✝ · `SimplexCategory)))
                          pure✝)
                        (matchExpr✝ (Expr.isConstOf✝ · `SSet)))
                      pure✝)
                    (matchExpr✝ (Expr.isConstOf✝ · `SSet.stdSimplex)))
                  (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `SimplexCategory.mk)) (matchVar✝ `n)) >=>
                pure✝)
              MatchState.empty✝ >>=
            fun s✝ => MatchState.delabVar✝ s✝ `n (some✝ e✝) >>= fun n => withHeadRefIfTagAppFns✝ `(Δ[$n]))
Похожие утверждения