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

Equations

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

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

Equations

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

structure Lean.Lsp.CompletionClientCapabilities : Type

• completionItem? : Option Lean.Lsp.CompletionItemCapabilities

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

Equations

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

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

Equations

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

structure Lean.Lsp.TextDocumentClientCapabilities : Type

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

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

Equations

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

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

Equations

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

structure Lean.Lsp.ShowDocumentClientCapabilities : Type

• support : Bool

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

Equations

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

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

Equations

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

structure Lean.Lsp.WindowClientCapabilities : Type

• showDocument? : Option Lean.Lsp.ShowDocumentClientCapabilities

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

Equations

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

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

Equations

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

structure Lean.Lsp.ChangeAnnotationSupport : Type

• groupsOnLabel? : Option Bool

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

Equations

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

instance Lean.Lsp.instFromJsonChangeAnnotationSupport : Lean.FromJson Lean.Lsp.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 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

Equations

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

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

Equations

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

structure Lean.Lsp.WorkspaceClientCapabilities : Type

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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