delabAdjoinNotation — Mathlib

Lean4
/-- Pretty printer for coercing schemes to types. -/
@[app_delab TopCat.carrier]
partial def delabAdjoinNotation : Delab :=
  whenPPOption getPPNotation do
    guard <| (← getExpr).isAppOfArity ``TopCat.carrier 1
    withNaryArg 0 do
        guard <| (← getExpr).isAppOfArity ``PresheafedSpace.carrier 3
        withNaryArg 2 do
            guard <| (← getExpr).isAppOfArity ``SheafedSpace.toPresheafedSpace 3
            withNaryArg 2 do
                guard <| (← getExpr).isAppOfArity ``LocallyRingedSpace.toSheafedSpace 1
                withNaryArg 0 do
                    guard <| (← getExpr).isAppOfArity ``Scheme.toLocallyRingedSpace 1
                    withNaryArg 0 do
                        `(↥$(← delab))
Похожие утверждения