Prod.fst や .snd のデラボレータを変更する例。[app_delab]使用例

Zulip: >
Infoview .1 and .2

import Mathlib.Tactic

variable (x : ℕ × ℕ)

#check x.1
#check x.fst

open Lean PrettyPrinter Delaborator
/-- Delaborator for `Prod.fst x` as `x.fst`. -/
@[app_delab Prod.fst]
def delabProdFst : Delab := withOverApp 3 do
  let x ← SubExpr.withAppArg delab
  `($(x).$(mkIdent `fst))

/-- Delaborator for `Prod.snd x` as `x.snd`. -/
@[app_delab Prod.snd]
def delabProdSnd : Delab := withOverApp 3 do
  let x ← SubExpr.withAppArg delab
  `($(x).$(mkIdent `snd))

#check x.1

#check x.2

Start with the Lean code example in the issue and inspect the repository's existing example pages to find the appropriate location. Done means the Prod.fst and Prod.snd @app_delab examples are included and the documentation build accepts the snippet.