From 60712815017fa0f33179c5424ca0aa10841f3605 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 26 Dec 2024 00:56:30 +0000 Subject: [PATCH 1/2] doc: explain `app_delab` --- src/Lean/PrettyPrinter/Delaborator/Basic.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean index a89ab65456a9..1b53ef0be147 100644 --- 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}'" From f5cd80af0293f22ec01124a56beeca0c8d80028f Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 28 Dec 2024 17:22:14 +0000 Subject: [PATCH 2/2] Update src/Lean/PrettyPrinter/Delaborator/Basic.lean Co-authored-by: Kyle Miller --- src/Lean/PrettyPrinter/Delaborator/Basic.lean | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) 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}'"