diff --git a/src/Lean/Server/Completion/CompletionUtils.lean b/src/Lean/Server/Completion/CompletionUtils.lean index 36af3aa6da..5b451f1ffd 100644 --- a/src/Lean/Server/Completion/CompletionUtils.lean +++ b/src/Lean/Server/Completion/CompletionUtils.lean @@ -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