Lean.Data.Lsp.Capabilities

source

structure Lean.Lsp.CompletionItemCapabilities :

Type

insertReplaceSupport? : Option Bool

source

instance Lean.Lsp.instToJsonCompletionItemCapabilities :

Lean.ToJson Lean.Lsp.CompletionItemCapabilities

Equations

Lean.Lsp.instToJsonCompletionItemCapabilities = { toJson := [anonymous] }

source

instance Lean.Lsp.instFromJsonCompletionItemCapabilities :

Lean.FromJson Lean.Lsp.CompletionItemCapabilities

Equations

Lean.Lsp.instFromJsonCompletionItemCapabilities = { fromJson? := [anonymous] }

source

structure Lean.Lsp.CompletionClientCapabilities :

Type

completionItem? : Option Lean.Lsp.CompletionItemCapabilities

source

instance Lean.Lsp.instToJsonCompletionClientCapabilities :

Lean.ToJson Lean.Lsp.CompletionClientCapabilities

Equations

Lean.Lsp.instToJsonCompletionClientCapabilities = { toJson := [anonymous] }

source

instance Lean.Lsp.instFromJsonCompletionClientCapabilities :

Lean.FromJson Lean.Lsp.CompletionClientCapabilities

Equations

Lean.Lsp.instFromJsonCompletionClientCapabilities = { fromJson? := [anonymous] }

source

structure Lean.Lsp.TextDocumentClientCapabilities :

Type

completion? : Option Lean.Lsp.CompletionClientCapabilities

source

instance Lean.Lsp.instFromJsonTextDocumentClientCapabilities :

Lean.FromJson Lean.Lsp.TextDocumentClientCapabilities

Equations

Lean.Lsp.instFromJsonTextDocumentClientCapabilities = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonTextDocumentClientCapabilities :

Lean.ToJson Lean.Lsp.TextDocumentClientCapabilities

Equations

Lean.Lsp.instToJsonTextDocumentClientCapabilities = { toJson := [anonymous] }

source

structure Lean.Lsp.ClientCapabilities :

Type

textDocument? : Option Lean.Lsp.TextDocumentClientCapabilities

source

instance Lean.Lsp.instToJsonClientCapabilities :

Lean.ToJson Lean.Lsp.ClientCapabilities

Equations

Lean.Lsp.instToJsonClientCapabilities = { toJson := [anonymous] }

source

instance Lean.Lsp.instFromJsonClientCapabilities :

Lean.FromJson Lean.Lsp.ClientCapabilities

Equations

Lean.Lsp.instFromJsonClientCapabilities = { fromJson? := [anonymous] }

source

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
semanticTokensProvider? : Option Lean.Lsp.SemanticTokensOptions

source

instance Lean.Lsp.instFromJsonServerCapabilities :

Lean.FromJson Lean.Lsp.ServerCapabilities

Equations

Lean.Lsp.instFromJsonServerCapabilities = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonServerCapabilities :

Lean.ToJson Lean.Lsp.ServerCapabilities

Equations

Lean.Lsp.instToJsonServerCapabilities = { toJson := [anonymous] }