doc: explain app_delab

leanprover · Dec 26, 2024 · 6071281 · 6071281
1 parent 0ebe9e5
commit 6071281
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -123,6 +123,11 @@ unsafe def mkDelabAttribute : IO (KeyedDeclsAttribute Delab) :=
   } `Lean.PrettyPrinter.Delaborator.delabAttribute
 @[builtin_init mkDelabAttribute] opaque delabAttribute : KeyedDeclsAttribute Delab
 
+/-- `@[app_delab c]` registers a declaration of type `Lean.PrettyPrinter.Delaborator.Delab` for applications
+of the constant `c` (including "nullary applications").
+
+It should be preferred over the otherwise-equivalent `@[delab app.c]`, as it first performs name-resolution
+on `c`. -/
 macro "app_delab" id:ident : attr => do
   match ← Macro.resolveGlobalName id.getId with
   | [] => Macro.throwErrorAt id s!"unknown declaration '{id.getId}'"