From 11eea84fd53481f1194b075d2a1ad7bff35a336d Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sun, 29 Dec 2024 15:06:55 +0000 Subject: [PATCH] doc: explain `app_delab` (#6450) This PR adds a docstring to the `@[app_delab]` attribute. --------- Co-authored-by: Kyle Miller --- src/Lean/PrettyPrinter/Delaborator/Basic.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean index a89ab65456a9..623ab4d2d1b1 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean @@ -123,6 +123,15 @@ unsafe def mkDelabAttribute : IO (KeyedDeclsAttribute Delab) := } `Lean.PrettyPrinter.Delaborator.delabAttribute @[builtin_init mkDelabAttribute] opaque delabAttribute : KeyedDeclsAttribute Delab +/-- +`@[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`. + +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}'"