max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: unknown identifier code actions with nested open (#10619)

Browse source 
This PR fixes a bug in the unknown identifier code actions where it
would yield non-sensical suggestions for nested `open` declarations like
`open Foo.Bar`.
This commit is contained in:
Marc Huisinga 2025-09-29 17:44:56 +02:00 • committed by GitHub
parent 76403367ba
commit 9f2ce635ae
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Server/Completion/CompletionUtils.lean
View file

@ -41,7 +41,7 @@ structure ContextualizedCompletionInfo where
ctx : ContextInfo
info : CompletionInfo
partial def minimizeGlobalIdentifierInContext (currNamespace : Name) (openDecls : List OpenDecl) (id : Name)
def minimizeGlobalIdentifierInContext (currNamespace : Name) (openDecls : List OpenDecl) (id : Name)
: Name := Id.run do
let mut minimized := shortenIn id currNamespace
for openDecl in openDecls do
@ -68,7 +68,7 @@ where
else if contextNamespace.isPrefixOf id then
id.replacePrefix contextNamespace .anonymous
else
shortenIn id contextNamespace.getPrefix
id
def unfoldDefinitionGuarded? (e : Expr) : MetaM (Option Expr) :=
try Lean.Meta.unfoldDefinition? e catch _ => pure none