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 : Lean.Name) : Lean.Lsp.CompletionIdentifier
• fvar (id : Lean.FVarId) : Lean.Lsp.CompletionIdentifier

instance Lean.Lsp.instFromJsonCompletionIdentifier : Lean.FromJson Lean.Lsp.CompletionIdentifier

Equations

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

instance Lean.Lsp.instToJsonCompletionIdentifier : Lean.ToJson Lean.Lsp.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 : Lean.Lsp.CompletionParams
• cPos : Nat

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

• id? : Option Lean.Lsp.CompletionIdentifier

instance Lean.Lsp.instFromJsonResolvableCompletionItemData : Lean.FromJson Lean.Lsp.ResolvableCompletionItemData

Equations

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

instance Lean.Lsp.instToJsonResolvableCompletionItemData : Lean.ToJson Lean.Lsp.ResolvableCompletionItemData

Equations

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

def Lean.Lsp.CompletionItem.resolve (item : Lean.Lsp.CompletionItem) (id : Lean.Lsp.CompletionIdentifier) : Lean.MetaM Lean.Lsp.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 : Lean.FileMap) (hoverPos : String.Pos) (cmdStx : Lean.Syntax) (infoTree : Lean.Elab.InfoTree) (item : Lean.Lsp.CompletionItem) (id : Lean.Lsp.CompletionIdentifier) (completionInfoPos : Nat) : IO Lean.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.