chore: use app_delab (#20249)

This has the same behavior as `delab app.`, but protects against typos. The feature appeared in leanprover/lean4#4976, though won't be documented until leanprover/lean4#6450.
leanprover-community · Dec 28, 2024 · aa72692 · aa72692
1 parent 9bfe1e0
commit aa72692
Show file tree

Hide file tree

Showing 14 changed files with 20 additions and 20 deletions.
diff --git a/Mathlib/Algebra/BigOperators/Expect.lean b/Mathlib/Algebra/BigOperators/Expect.lean
@@ -85,7 +85,7 @@ open Batteries.ExtendedBinder
 
 /-- Delaborator for `Finset.expect`. The `pp.piBinderTypes` option controls whether
 to show the domain type when the expect is over `Finset.univ`. -/
-@[scoped delab app.Finset.expect] def delabFinsetExpect : Delab :=
+@[scoped app_delab Finset.expect] def delabFinsetExpect : Delab :=
   whenPPOption getPPNotation <| withOverApp 6 <| do
   let #[_, _, _, _, s, f] := (← getExpr).getAppArgs | failure
   guard <| f.isLambda

diff --git a/Mathlib/Algebra/BigOperators/Group/Finset.lean b/Mathlib/Algebra/BigOperators/Group/Finset.lean
@@ -218,7 +218,7 @@ open scoped Batteries.ExtendedBinder
 
 /-- Delaborator for `Finset.prod`. The `pp.piBinderTypes` option controls whether
 to show the domain type when the product is over `Finset.univ`. -/
-@[delab app.Finset.prod] def delabFinsetProd : Delab :=
+@[app_delab Finset.prod] def delabFinsetProd : Delab :=
   whenPPOption getPPNotation <| withOverApp 5 <| do
   let #[_, _, _, s, f] := (← getExpr).getAppArgs | failure
   guard <| f.isLambda
@@ -239,7 +239,7 @@ to show the domain type when the product is over `Finset.univ`. -/
 
 /-- Delaborator for `Finset.sum`. The `pp.piBinderTypes` option controls whether
 to show the domain type when the sum is over `Finset.univ`. -/
-@[delab app.Finset.sum] def delabFinsetSum : Delab :=
+@[app_delab Finset.sum] def delabFinsetSum : Delab :=
   whenPPOption getPPNotation <| withOverApp 5 <| do
   let #[_, _, _, s, f] := (← getExpr).getAppArgs | failure
   guard <| f.isLambda

diff --git a/Mathlib/Analysis/InnerProductSpace/PiL2.lean b/Mathlib/Analysis/InnerProductSpace/PiL2.lean
@@ -119,7 +119,7 @@ macro_rules | `(!$p:subscript[$e:term,*]) => do
 
 set_option trace.debug true in
 /-- Unexpander for the `!₂[x, y, ...]` notation. -/
-@[delab app.DFunLike.coe]
+@[app_delab DFunLike.coe]
 def EuclideanSpace.delabVecNotation : Delab :=
   whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <| withOverApp 6 do
     -- check that the `(WithLp.equiv _ _).symm` is present

diff --git a/Mathlib/CategoryTheory/Closed/Cartesian.lean b/Mathlib/CategoryTheory/Closed/Cartesian.lean
@@ -117,7 +117,7 @@ notation:20 A " ⟹ " B:19 => (exp A).obj B
 
 open Lean PrettyPrinter.Delaborator SubExpr in
 /-- Delaborator for `Prefunctor.obj` -/
-@[delab app.Prefunctor.obj]
+@[app_delab Prefunctor.obj]
 def delabPrefunctorObjExp : Delab := whenPPOption getPPNotation <| withOverApp 6 <| do
   let e ← getExpr
   guard <| e.isAppOfArity' ``Prefunctor.obj 6

diff --git a/Mathlib/CategoryTheory/Monoidal/Category.lean b/Mathlib/CategoryTheory/Monoidal/Category.lean
@@ -124,7 +124,7 @@ scoped notation "𝟙_ " C:max => (MonoidalCategoryStruct.tensorUnit : C)
 
 open Lean PrettyPrinter.Delaborator SubExpr in
 /-- Used to ensure that `𝟙_` notation is used, as the ascription makes this not automatic. -/
-@[delab app.CategoryTheory.MonoidalCategoryStruct.tensorUnit]
+@[app_delab CategoryTheory.MonoidalCategoryStruct.tensorUnit]
 def delabTensorUnit : Delab := whenPPOption getPPNotation <| withOverApp 3 do
   let e ← getExpr
   guard <| e.isAppOfArity ``MonoidalCategoryStruct.tensorUnit 3

diff --git a/Mathlib/Data/Matrix/Notation.lean b/Mathlib/Data/Matrix/Notation.lean
@@ -111,7 +111,7 @@ macro_rules
   | `(!![$[,%$commas]*]) => `(@Matrix.of (Fin 0) (Fin $(quote commas.size)) _ ![])
 
 /-- Delaborator for the `!![]` notation. -/
-@[delab app.DFunLike.coe]
+@[app_delab DFunLike.coe]
 def delabMatrixNotation : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <|
   withOverApp 6 do
     let mkApp3 (.const ``Matrix.of _) (.app (.const ``Fin _) em) (.app (.const ``Fin _) en) _ :=

diff --git a/Mathlib/Data/Prod/Basic.lean b/Mathlib/Data/Prod/Basic.lean
@@ -304,13 +304,13 @@ section delaborators
 open Lean PrettyPrinter Delaborator
 
 /-- Delaborator for `Prod.fst x` as `x.1`. -/
-@[delab app.Prod.fst]
+@[app_delab Prod.fst]
 def delabProdFst : Delab := withOverApp 3 do
   let x ← SubExpr.withAppArg delab
   `($(x).1)
 
 /-- Delaborator for `Prod.snd x` as `x.2`. -/
-@[delab app.Prod.snd]
+@[app_delab Prod.snd]
 def delabProdSnd : Delab := withOverApp 3 do
   let x ← SubExpr.withAppArg delab
   `($(x).2)

diff --git a/Mathlib/Data/SetLike/Basic.lean b/Mathlib/Data/SetLike/Basic.lean
@@ -117,7 +117,7 @@ open Lean PrettyPrinter.Delaborator SubExpr
 /-- For terms that match the `CoeSort` instance's body, pretty print as `↥S`
 rather than as `{ x // x ∈ S }`. The discriminating feature is that membership
 uses the `SetLike.instMembership` instance. -/
-@[delab app.Subtype]
+@[app_delab Subtype]
 def delabSubtypeSetLike : Delab := whenPPOption getPPNotation do
   let #[_, .lam n _ body _] := (← getExpr).getAppArgs | failure
   guard <| body.isAppOf ``Membership.mem

diff --git a/Mathlib/FieldTheory/Adjoin.lean b/Mathlib/FieldTheory/Adjoin.lean
@@ -600,7 +600,7 @@ generated by these elements. -/
 scoped macro:max K:term "⟮" xs:term,* "⟯" : term => do ``(adjoin $K $(← mkInsertTerm xs.getElems))
 
 open Lean PrettyPrinter.Delaborator SubExpr in
-@[delab app.IntermediateField.adjoin]
+@[app_delab IntermediateField.adjoin]
 partial def delabAdjoinNotation : Delab := whenPPOption getPPNotation do
   let e ← getExpr
   guard <| e.isAppOfArity ``adjoin 6

diff --git a/Mathlib/LinearAlgebra/LinearIndependent.lean b/Mathlib/LinearAlgebra/LinearIndependent.lean
@@ -109,7 +109,7 @@ in case the family of vectors is over a `Set`.
 
 Type hints look like `LinearIndependent fun (v : ↑s) => ↑v` or `LinearIndependent (ι := ↑s) f`,
 depending on whether the family is a lambda expression or not. -/
-@[delab app.LinearIndependent]
+@[app_delab LinearIndependent]
 def delabLinearIndependent : Delab :=
   whenPPOption getPPNotation <|
   whenNotPPOption getPPAnalysisSkip <|

diff --git a/Mathlib/LinearAlgebra/Matrix/PosDef.lean b/Mathlib/LinearAlgebra/Matrix/PosDef.lean
@@ -172,7 +172,7 @@ noncomputable def sqrt : Matrix n n 𝕜 :=
 
 open Lean PrettyPrinter.Delaborator SubExpr in
 /-- Custom elaborator to produce output like `(_ : PosSemidef A).sqrt` in the goal view. -/
-@[delab app.Matrix.PosSemidef.sqrt]
+@[app_delab Matrix.PosSemidef.sqrt]
 def delabSqrt : Delab :=
   whenPPOption getPPNotation <|
   whenNotPPOption getPPAnalysisSkip <|

diff --git a/Mathlib/Order/SetNotation.lean b/Mathlib/Order/SetNotation.lean
@@ -88,7 +88,7 @@ section delaborators
 open Lean Lean.PrettyPrinter.Delaborator
 
 /-- Delaborator for indexed supremum. -/
-@[delab app.iSup]
+@[app_delab iSup]
 def iSup_delab : Delab := whenPPOption Lean.getPPNotation <| withOverApp 4 do
   let #[_, ι, _, f] := (← SubExpr.getExpr).getAppArgs | failure
   unless f.isLambda do failure
@@ -116,7 +116,7 @@ def iSup_delab : Delab := whenPPOption Lean.getPPNotation <| withOverApp 4 do
   return stx
 
 /-- Delaborator for indexed infimum. -/
-@[delab app.iInf]
+@[app_delab iInf]
 def iInf_delab : Delab := whenPPOption Lean.getPPNotation <| withOverApp 4 do
   let #[_, ι, _, f] := (← SubExpr.getExpr).getAppArgs | failure
   unless f.isLambda do failure
@@ -193,7 +193,7 @@ section delaborators
 open Lean Lean.PrettyPrinter.Delaborator
 
 /-- Delaborator for indexed unions. -/
-@[delab app.Set.iUnion]
+@[app_delab Set.iUnion]
 def iUnion_delab : Delab := whenPPOption Lean.getPPNotation do
   let #[_, ι, f] := (← SubExpr.getExpr).getAppArgs | failure
   unless f.isLambda do failure
@@ -221,7 +221,7 @@ def iUnion_delab : Delab := whenPPOption Lean.getPPNotation do
   return stx
 
 /-- Delaborator for indexed intersections. -/
-@[delab app.Set.iInter]
+@[app_delab Set.iInter]
 def sInter_delab : Delab := whenPPOption Lean.getPPNotation do
   let #[_, ι, f] := (← SubExpr.getExpr).getAppArgs | failure
   unless f.isLambda do failure

diff --git a/Mathlib/RingTheory/Derivation/DifferentialRing.lean b/Mathlib/RingTheory/Derivation/DifferentialRing.lean
@@ -27,7 +27,7 @@ open Lean PrettyPrinter Delaborator SubExpr in
 A delaborator for the x′ notation. This is required because it's not direct function application,
 so the default delaborator doesn't work.
 -/
-@[delab app.DFunLike.coe]
+@[app_delab DFunLike.coe]
 def delabDeriv : Delab := do
   let e ← getExpr
   guard <| e.isAppOfArity' ``DFunLike.coe 6

diff --git a/Mathlib/Util/Delaborators.lean b/Mathlib/Util/Delaborators.lean
@@ -97,7 +97,7 @@ open Lean Parser Term PrettyPrinter Delaborator
 
 /-- Delaborator for existential quantifier, including extended binders. -/
 -- TODO: reduce the duplication in this code
-@[delab app.Exists]
+@[app_delab Exists]
 def exists_delab : Delab := whenPPOption Lean.getPPNotation do
   let #[ι, f] := (← SubExpr.getExpr).getAppArgs | failure
   unless f.isLambda do failure
@@ -159,7 +159,7 @@ end existential
 open Lean Lean.PrettyPrinter.Delaborator
 
 /-- Delaborator for `∉`. -/
-@[delab app.Not] def delab_not_in := whenPPOption Lean.getPPNotation do
+@[app_delab Not] def delab_not_in := whenPPOption Lean.getPPNotation do
   let #[f] := (← SubExpr.getExpr).getAppArgs | failure
   guard <| f.isAppOfArity ``Membership.mem 5
   let stx₁ ← SubExpr.withAppArg <| SubExpr.withNaryArg 3 delab