inductive Lean.Lsp.CompletionIdentifier : Type

Identifier that is sent from the server to the client as part of the CompletionItem.data? field. Needed to resolve the CompletionItem when the client sends a completionItem/resolve request for that item, again containing the data? field provided by the server.

• const (declName : Name) : CompletionIdentifier
• fvar (id : FVarId) : CompletionIdentifier

instance Lean.Lsp.instFromJsonCompletionIdentifier : FromJson CompletionIdentifier

Equations

• Lean.Lsp.instFromJsonCompletionIdentifier = { fromJson? := Lean.Lsp.fromJsonCompletionIdentifier✝ }

instance Lean.Lsp.instToJsonCompletionIdentifier : ToJson CompletionIdentifier

Equations

• Lean.Lsp.instToJsonCompletionIdentifier = { toJson := Lean.Lsp.toJsonCompletionIdentifier✝ }

structure Lean.Lsp.ResolvableCompletionItemDataextends Lean.Lsp.CompletionItemData : Type

CompletionItemData that contains additional information to identify the item in order to resolve it.

• params : CompletionParams
• cPos : Nat

  Position of the completion info that this completion item was created from.

• id? : Option CompletionIdentifier

instance Lean.Lsp.instFromJsonResolvableCompletionItemData : FromJson ResolvableCompletionItemData

Equations

• Lean.Lsp.instFromJsonResolvableCompletionItemData = { fromJson? := Lean.Lsp.fromJsonResolvableCompletionItemData✝ }

instance Lean.Lsp.instToJsonResolvableCompletionItemData : ToJson ResolvableCompletionItemData

Equations

• Lean.Lsp.instToJsonResolvableCompletionItemData = { toJson := Lean.Lsp.toJsonResolvableCompletionItemData✝ }

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.

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.