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 : Lean.ToJson Lean.Lsp.CompletionItemCapabilities

instance Lean.Lsp.instFromJsonCompletionItemCapabilities : Lean.FromJson Lean.Lsp.CompletionItemCapabilities

structure Lean.Lsp.CompletionClientCapabilities : Type

• completionItem? : Option Lean.Lsp.CompletionItemCapabilities

instance Lean.Lsp.instToJsonCompletionClientCapabilities : Lean.ToJson Lean.Lsp.CompletionClientCapabilities

instance Lean.Lsp.instFromJsonCompletionClientCapabilities : Lean.FromJson Lean.Lsp.CompletionClientCapabilities

structure Lean.Lsp.TextDocumentClientCapabilities : Type

• completion? : Option Lean.Lsp.CompletionClientCapabilities
• codeAction? : Option Lean.Lsp.CodeActionClientCapabilities

instance Lean.Lsp.instToJsonTextDocumentClientCapabilities : Lean.ToJson Lean.Lsp.TextDocumentClientCapabilities

instance Lean.Lsp.instFromJsonTextDocumentClientCapabilities : Lean.FromJson Lean.Lsp.TextDocumentClientCapabilities

structure Lean.Lsp.ShowDocumentClientCapabilities : Type

• support : Bool

instance Lean.Lsp.instToJsonShowDocumentClientCapabilities : Lean.ToJson Lean.Lsp.ShowDocumentClientCapabilities

instance Lean.Lsp.instFromJsonShowDocumentClientCapabilities : Lean.FromJson Lean.Lsp.ShowDocumentClientCapabilities

structure Lean.Lsp.WindowClientCapabilities : Type

• showDocument? : Option Lean.Lsp.ShowDocumentClientCapabilities

instance Lean.Lsp.instToJsonWindowClientCapabilities : Lean.ToJson Lean.Lsp.WindowClientCapabilities

instance Lean.Lsp.instFromJsonWindowClientCapabilities : Lean.FromJson Lean.Lsp.WindowClientCapabilities

structure Lean.Lsp.ChangeAnnotationSupport : Type

• groupsOnLabel? : Option Bool

instance Lean.Lsp.instToJsonChangeAnnotationSupport : Lean.ToJson Lean.Lsp.ChangeAnnotationSupport

instance Lean.Lsp.instFromJsonChangeAnnotationSupport : Lean.FromJson Lean.Lsp.ChangeAnnotationSupport

structure Lean.Lsp.WorkspaceEditClientCapabilities : Type

• documentChanges? : Option Bool

  The client supports versioned document changes in WorkspaceEdits.

• changeAnnotationSupport? : Option Lean.Lsp.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 : Lean.ToJson Lean.Lsp.WorkspaceEditClientCapabilities

instance Lean.Lsp.instFromJsonWorkspaceEditClientCapabilities : Lean.FromJson Lean.Lsp.WorkspaceEditClientCapabilities

structure Lean.Lsp.WorkspaceClientCapabilities : Type

• applyEdit : Bool
• workspaceEdit? : Option Lean.Lsp.WorkspaceEditClientCapabilities

instance Lean.Lsp.instToJsonWorkspaceClientCapabilities : Lean.ToJson Lean.Lsp.WorkspaceClientCapabilities

instance Lean.Lsp.instFromJsonWorkspaceClientCapabilities : Lean.FromJson Lean.Lsp.WorkspaceClientCapabilities

structure Lean.Lsp.ClientCapabilities : Type

• textDocument? : Option Lean.Lsp.TextDocumentClientCapabilities
• window? : Option Lean.Lsp.WindowClientCapabilities
• workspace? : Option Lean.Lsp.WorkspaceClientCapabilities

instance Lean.Lsp.instToJsonClientCapabilities : Lean.ToJson Lean.Lsp.ClientCapabilities

instance Lean.Lsp.instFromJsonClientCapabilities : Lean.FromJson Lean.Lsp.ClientCapabilities

structure Lean.Lsp.ServerCapabilities : Type

• textDocumentSync? : Option Lean.Lsp.TextDocumentSyncOptions
• completionProvider? : Option Lean.Lsp.CompletionOptions
• hoverProvider : Bool
• documentHighlightProvider : Bool
• documentSymbolProvider : Bool
• definitionProvider : Bool
• declarationProvider : Bool
• typeDefinitionProvider : Bool
• referencesProvider : Bool
• workspaceSymbolProvider : Bool
• foldingRangeProvider : Bool
• semanticTokensProvider? : Option Lean.Lsp.SemanticTokensOptions
• codeActionProvider? : Option Lean.Lsp.CodeActionOptions

instance Lean.Lsp.instToJsonServerCapabilities : Lean.ToJson Lean.Lsp.ServerCapabilities

instance Lean.Lsp.instFromJsonServerCapabilities : Lean.FromJson Lean.Lsp.ServerCapabilities