Documentation

Lean.Server.Completion.CompletionResolution

source
def Lean.Lsp.CompletionItem.resolve (item : CompletionItem) (id : CompletionIdentifier) :
MetaM CompletionItem

Fills the CompletionItem.detail? field of item using the pretty-printed type identified by id.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Server.Completion.resolveCompletionItem? (fileMap : FileMap) (hoverPos : String.Pos) (cmdStx : Syntax) (infoTree : Elab.InfoTree) (item : Lsp.CompletionItem) (id : Lsp.CompletionIdentifier) (completionInfoPos : Nat) :
    IO Lsp.CompletionItem

    Fills the CompletionItem.detail? field of item using the pretty-printed type identified by id in the context found at hoverPos in infoTree.

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