Minimal LSP servers/clients do not have to implement a lot of functionality. Most useful additional behavior is instead opted into via capabilities.

structure Lean.Lsp.CompletionItemCapabilities : Type

• insertReplaceSupport? : Option Bool

instance Lean.Lsp.instToJsonCompletionItemCapabilities : ToJson CompletionItemCapabilities

Equations

• Lean.Lsp.instToJsonCompletionItemCapabilities = { toJson := Lean.Lsp.toJsonCompletionItemCapabilities✝ }

instance Lean.Lsp.instFromJsonCompletionItemCapabilities : FromJson CompletionItemCapabilities

Equations

• Lean.Lsp.instFromJsonCompletionItemCapabilities = { fromJson? := Lean.Lsp.fromJsonCompletionItemCapabilities✝ }

structure Lean.Lsp.CompletionClientCapabilities : Type

• completionItem? : Option CompletionItemCapabilities

instance Lean.Lsp.instToJsonCompletionClientCapabilities : ToJson CompletionClientCapabilities

Equations

• Lean.Lsp.instToJsonCompletionClientCapabilities = { toJson := Lean.Lsp.toJsonCompletionClientCapabilities✝ }

instance Lean.Lsp.instFromJsonCompletionClientCapabilities : FromJson CompletionClientCapabilities

Equations

• Lean.Lsp.instFromJsonCompletionClientCapabilities = { fromJson? := Lean.Lsp.fromJsonCompletionClientCapabilities✝ }

structure Lean.Lsp.TextDocumentClientCapabilities : Type

• completion? : Option CompletionClientCapabilities
• codeAction? : Option CodeActionClientCapabilities
• inlayHint? : Option InlayHintClientCapabilities

instance Lean.Lsp.instToJsonTextDocumentClientCapabilities : ToJson TextDocumentClientCapabilities

Equations

• Lean.Lsp.instToJsonTextDocumentClientCapabilities = { toJson := Lean.Lsp.toJsonTextDocumentClientCapabilities✝ }

instance Lean.Lsp.instFromJsonTextDocumentClientCapabilities : FromJson TextDocumentClientCapabilities

Equations

• Lean.Lsp.instFromJsonTextDocumentClientCapabilities = { fromJson? := Lean.Lsp.fromJsonTextDocumentClientCapabilities✝ }

structure Lean.Lsp.ShowDocumentClientCapabilities : Type

• support : Bool

instance Lean.Lsp.instToJsonShowDocumentClientCapabilities : ToJson ShowDocumentClientCapabilities

Equations

• Lean.Lsp.instToJsonShowDocumentClientCapabilities = { toJson := Lean.Lsp.toJsonShowDocumentClientCapabilities✝ }

instance Lean.Lsp.instFromJsonShowDocumentClientCapabilities : FromJson ShowDocumentClientCapabilities

Equations

• Lean.Lsp.instFromJsonShowDocumentClientCapabilities = { fromJson? := Lean.Lsp.fromJsonShowDocumentClientCapabilities✝ }

structure Lean.Lsp.WindowClientCapabilities : Type

• showDocument? : Option ShowDocumentClientCapabilities

instance Lean.Lsp.instToJsonWindowClientCapabilities : ToJson WindowClientCapabilities

Equations

• Lean.Lsp.instToJsonWindowClientCapabilities = { toJson := Lean.Lsp.toJsonWindowClientCapabilities✝ }

instance Lean.Lsp.instFromJsonWindowClientCapabilities : FromJson WindowClientCapabilities

Equations

• Lean.Lsp.instFromJsonWindowClientCapabilities = { fromJson? := Lean.Lsp.fromJsonWindowClientCapabilities✝ }

structure Lean.Lsp.ChangeAnnotationSupport : Type

• groupsOnLabel? : Option Bool

instance Lean.Lsp.instToJsonChangeAnnotationSupport : ToJson ChangeAnnotationSupport

Equations

• Lean.Lsp.instToJsonChangeAnnotationSupport = { toJson := Lean.Lsp.toJsonChangeAnnotationSupport✝ }

instance Lean.Lsp.instFromJsonChangeAnnotationSupport : FromJson ChangeAnnotationSupport

Equations

• Lean.Lsp.instFromJsonChangeAnnotationSupport = { fromJson? := Lean.Lsp.fromJsonChangeAnnotationSupport✝ }

structure Lean.Lsp.WorkspaceEditClientCapabilities : Type

• documentChanges? : Option Bool

  The client supports versioned document changes in WorkspaceEdits.

• changeAnnotationSupport? : Option ChangeAnnotationSupport

  Whether the client in general supports change annotations on text edits.

• resourceOperations? : Option (Array String)

  The resource operations the client supports. Clients should at least support 'create', 'rename' and 'delete' files and folders.

instance Lean.Lsp.instToJsonWorkspaceEditClientCapabilities : ToJson WorkspaceEditClientCapabilities

Equations

• Lean.Lsp.instToJsonWorkspaceEditClientCapabilities = { toJson := Lean.Lsp.toJsonWorkspaceEditClientCapabilities✝ }

instance Lean.Lsp.instFromJsonWorkspaceEditClientCapabilities : FromJson WorkspaceEditClientCapabilities

Equations

• Lean.Lsp.instFromJsonWorkspaceEditClientCapabilities = { fromJson? := Lean.Lsp.fromJsonWorkspaceEditClientCapabilities✝ }

structure Lean.Lsp.WorkspaceClientCapabilities : Type

• applyEdit? : Option Bool
• workspaceEdit? : Option WorkspaceEditClientCapabilities

instance Lean.Lsp.instToJsonWorkspaceClientCapabilities : ToJson WorkspaceClientCapabilities

Equations

• Lean.Lsp.instToJsonWorkspaceClientCapabilities = { toJson := Lean.Lsp.toJsonWorkspaceClientCapabilities✝ }

instance Lean.Lsp.instFromJsonWorkspaceClientCapabilities : FromJson WorkspaceClientCapabilities

Equations

• Lean.Lsp.instFromJsonWorkspaceClientCapabilities = { fromJson? := Lean.Lsp.fromJsonWorkspaceClientCapabilities✝ }

structure Lean.Lsp.LeanClientCapabilities : Type

• silentDiagnosticSupport? : Option Bool

  Whether the client supports DiagnosticWith.isSilent = true. If none or false, silent diagnostics will not be served to the client.

instance Lean.Lsp.instToJsonLeanClientCapabilities : ToJson LeanClientCapabilities

Equations

• Lean.Lsp.instToJsonLeanClientCapabilities = { toJson := Lean.Lsp.toJsonLeanClientCapabilities✝ }

instance Lean.Lsp.instFromJsonLeanClientCapabilities : FromJson LeanClientCapabilities

Equations

• Lean.Lsp.instFromJsonLeanClientCapabilities = { fromJson? := Lean.Lsp.fromJsonLeanClientCapabilities✝ }

structure Lean.Lsp.ClientCapabilities : Type

• textDocument? : Option TextDocumentClientCapabilities
• window? : Option WindowClientCapabilities
• workspace? : Option WorkspaceClientCapabilities
• lean? : Option LeanClientCapabilities

  Capabilties for Lean language server extensions.

instance Lean.Lsp.instToJsonClientCapabilities : ToJson ClientCapabilities

Equations

• Lean.Lsp.instToJsonClientCapabilities = { toJson := Lean.Lsp.toJsonClientCapabilities✝ }

instance Lean.Lsp.instFromJsonClientCapabilities : FromJson ClientCapabilities

Equations

• Lean.Lsp.instFromJsonClientCapabilities = { fromJson? := Lean.Lsp.fromJsonClientCapabilities✝ }

def Lean.Lsp.ClientCapabilities.silentDiagnosticSupport (c : ClientCapabilities) : Bool

Equations

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

structure Lean.Lsp.ServerCapabilities : Type

• textDocumentSync? : Option TextDocumentSyncOptions
• completionProvider? : Option CompletionOptions
• hoverProvider : Bool
• documentHighlightProvider : Bool
• documentSymbolProvider : Bool
• definitionProvider : Bool
• declarationProvider : Bool
• typeDefinitionProvider : Bool
• referencesProvider : Bool
• callHierarchyProvider : Bool
• renameProvider? : Option RenameOptions
• workspaceSymbolProvider : Bool
• foldingRangeProvider : Bool
• semanticTokensProvider? : Option SemanticTokensOptions
• codeActionProvider? : Option CodeActionOptions
• inlayHintProvider? : Option InlayHintOptions

instance Lean.Lsp.instToJsonServerCapabilities : ToJson ServerCapabilities

Equations

• Lean.Lsp.instToJsonServerCapabilities = { toJson := Lean.Lsp.toJsonServerCapabilities✝ }

instance Lean.Lsp.instFromJsonServerCapabilities : FromJson ServerCapabilities

Equations

• Lean.Lsp.instFromJsonServerCapabilities = { fromJson? := Lean.Lsp.fromJsonServerCapabilities✝ }