def Lean.getSuggestions {m : Type → Type} [Monad m] [MonadEnv m] (incorrectName : Name) : m NameSet

Given a name, find all the stored correct, existing identifiers that mention that name in a suggest_for annotation.

def Lean.getStoredSuggestions {m : Type → Type} [Monad m] [MonadEnv m] (trueName : Name) : m NameSet

Given a (presumably existing) identifier, find all the suggest_for annotations that were given for that identifier.

def Lean.throwUnknownNameWithSuggestions {α : Type} (constName : Name) (idOrConst : String := "identifier") (declHint : Name := constName) (ref? : Option Syntax := none) (extraMsg : MessageData := MessageData.nil) : Elab.TermElabM α

Throw an unknown constant/identifier error message, potentially suggesting alternatives using suggest_for attributes.

The replacement will mimic the path structure of the original as much as possible if they share a path prefix: if there is a suggestion for replacing Foo.Bar.jazz with Foo.Bar.baz, then Bar.jazz will be replaced by Bar.baz unless the resulting constant is ambiguous.

def Lean.Elab.Term.hintAutoImplicitFailure (exp : Expr) (expected : String := "a function") : TermElabM MessageData