This exports a predicate for checking whether a name should be made visible in auto-completion and other tactics that suggest names to insert into Lean code.

The exact? tactic is an example of a tactic that benefits from this functionality. exact? finds lemmas in the environment to use to prove a theorem, but it needs to avoid inserting references to theorems with unstable names such as auxillary lemmas that could change with minor unintentional modifications to definitions.

It uses a blacklist environment extension to enable names in an environment to be specifically hidden.

opaque Lean.Meta.completionBlackListExt : Lean.TagDeclarationExtension

@[export lean_completion_add_to_black_list]

def Lean.Meta.addToCompletionBlackList (env : Lean.Environment) (declName : Lake.Name) : Lean.Environment

Equations

• Lean.Meta.addToCompletionBlackList env declName = Lean.Meta.completionBlackListExt.tag env declName

def Lean.Meta.allowCompletion (env : Lean.Environment) (declName : Lake.Name) : Bool

Return true if completion is allowed for name.

Equations

• Lean.Meta.allowCompletion env declName = !Lean.Meta.isBlacklisted env declName