diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index 1b53ef0be147..623ab4d2d1b1 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -123,11 +123,15 @@ 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").
+/--
+`@[app_delab c]` registers a delaborator for applications with head constant `c`.
+Such delaborators also apply to the constant `c` itself (known as a "nullary application").
+
+This attribute should be applied to definitions of type `Lean.PrettyPrinter.Delaborator.Delab`.
 
-It should be preferred over the otherwise-equivalent `@[delab app.c]`, as it first performs name-resolution
-on `c`. -/
+When defining delaborators for constant applications, one should prefer this attribute over `@[delab app.c]`,
+as `@[app_delab c]` first performs name resolution on `c` in the current scope.
+-/
 macro "app_delab" id:ident : attr => do
   match ← Macro.resolveGlobalName id.getId with
   | [] => Macro.throwErrorAt id s!"unknown declaration '{id.getId}'"