From 9001fcf317863f31b8a01f65681e10776b6c9552 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sat, 29 Aug 2026 11:16:43 -0700 Subject: [PATCH] feat: completions for `@[delab app.foo]` attribute This PR adds completions to the `@[delab]` attribute for the `app` prefix. --- src/Lean/PrettyPrinter/Delaborator/Basic.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean index 291d618e54e6..e87733225cc6 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean @@ -118,11 +118,14 @@ unsafe builtin_initialize delabAttribute : KeyedDeclsAttribute Delab ← evalKey := fun _ stx => do let stx ← Attribute.Builtin.getIdent stx let kind := stx.getId - if (← Elab.getInfoState).enabled && kind.getRoot == `app then + if (← Elab.getInfoState).enabled && !kind.isAtomic && kind.getRoot == `app then let c := kind.replacePrefix `app .anonymous + -- Create identifier dropping `app` prefix, for completions and term info + let stx' := mkIdentFrom (mkNullNode (Syntax.identComponents stx).tail.toArray) c (canonical := true) + Elab.addCompletionInfo <| .id stx' c (danglingDot := false) (lctx := {}) (expectedType? := none) if (← getEnv).contains c then recordExtraModUseFromDecl (isMeta := false) c - Elab.addConstInfo stx c none + Elab.addConstInfo stx' c none pure kind }