def Lean.Server.Completion.findCompletionInfosAt (fileMap : Lean.FileMap) (hoverPos : String.Pos) (cmdStx : Lean.Syntax) (infoTree : Lean.Elab.InfoTree) : Array Lean.Server.Completion.ContextualizedCompletionInfo

Equations

• One or more equations did not get rendered due to their size.

def Lean.Server.Completion.findCompletionInfosAt.go (fileMap : Lean.FileMap) (hoverPos : String.Pos) (hoverLine : Nat) (ctx : Lean.Elab.ContextInfo) (info : Lean.Elab.Info) (best : Array Lean.Server.Completion.ContextualizedCompletionInfo) : Array Lean.Server.Completion.ContextualizedCompletionInfo

Equations

• One or more equations did not get rendered due to their size.
• Lean.Server.Completion.findCompletionInfosAt.go fileMap hoverPos hoverLine ctx info best = (pure best).run

def Lean.Server.Completion.findPrioritizedCompletionPartitionsAt (fileMap : Lean.FileMap) (hoverPos : String.Pos) (cmdStx : Lean.Syntax) (infoTree : Lean.Elab.InfoTree) : Array (Array (Lean.Server.Completion.ContextualizedCompletionInfo × Nat))

Finds all CompletionInfos (both from the InfoTree and synthetic ones), prioritizes them, arranges them in partitions of CompletionInfos with the same priority and sorts these partitions so that CompletionInfos with the highest priority come first. The returned CompletionInfos are also tagged with their index in findCompletionInfosAt so that when resolving a CompletionItem, we can reconstruct which CompletionInfo it was created from.

In general, the InfoTree may contain multiple different CompletionInfos covering hoverPos, and so we need to decide which of these CompletionInfos we want to use to show completions to the user. We choose priorities by the following rules:

• Synthetic completions have the lowest priority since they are only intended as a backup.
• Non-identifier completions have the highest priority since they tend to be much more helpful than identifier completions when available since there are typically way too many of the latter.
• Within the three groups [non-id completions, id completions, synthetic completions], CompletionInfos with a smaller range are considered to be better.

Equations

• One or more equations did not get rendered due to their size.