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

def Lean.Lsp.instToJsonCompletionItemCapabilities.toJson : CompletionItemCapabilities → Json

Equations

• Lean.Lsp.instToJsonCompletionItemCapabilities.toJson x✝ = Lean.Json.mkObj [Lean.Json.opt "insertReplaceSupport" x✝.insertReplaceSupport?].flatten

instance Lean.Lsp.instToJsonCompletionItemCapabilities : ToJson CompletionItemCapabilities

Equations

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

def Lean.Lsp.instFromJsonCompletionItemCapabilities.fromJson : Json → Except String CompletionItemCapabilities

Equations

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

instance Lean.Lsp.instFromJsonCompletionItemCapabilities : FromJson CompletionItemCapabilities

Equations

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

structure Lean.Lsp.CompletionClientCapabilities : Type

• completionItem? : Option CompletionItemCapabilities

def Lean.Lsp.instToJsonCompletionClientCapabilities.toJson : CompletionClientCapabilities → Json

Equations

• Lean.Lsp.instToJsonCompletionClientCapabilities.toJson x✝ = Lean.Json.mkObj [Lean.Json.opt "completionItem" x✝.completionItem?].flatten

instance Lean.Lsp.instToJsonCompletionClientCapabilities : ToJson CompletionClientCapabilities

Equations

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

def Lean.Lsp.instFromJsonCompletionClientCapabilities.fromJson : Json → Except String CompletionClientCapabilities

Equations

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

instance Lean.Lsp.instFromJsonCompletionClientCapabilities : FromJson CompletionClientCapabilities

Equations

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

structure Lean.Lsp.TextDocumentClientCapabilities : Type

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

def Lean.Lsp.instToJsonTextDocumentClientCapabilities.toJson : TextDocumentClientCapabilities → Json

Equations

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

instance Lean.Lsp.instToJsonTextDocumentClientCapabilities : ToJson TextDocumentClientCapabilities

Equations

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

def Lean.Lsp.instFromJsonTextDocumentClientCapabilities.fromJson : Json → Except String TextDocumentClientCapabilities

Equations

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

instance Lean.Lsp.instFromJsonTextDocumentClientCapabilities : FromJson TextDocumentClientCapabilities

Equations

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

structure Lean.Lsp.ShowDocumentClientCapabilities : Type

• support : Bool

instance Lean.Lsp.instToJsonShowDocumentClientCapabilities : ToJson ShowDocumentClientCapabilities

Equations

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

def Lean.Lsp.instToJsonShowDocumentClientCapabilities.toJson : ShowDocumentClientCapabilities → Json

Equations

• Lean.Lsp.instToJsonShowDocumentClientCapabilities.toJson x✝ = Lean.Json.mkObj [[("support", Lean.toJson x✝.support)]].flatten

instance Lean.Lsp.instFromJsonShowDocumentClientCapabilities : FromJson ShowDocumentClientCapabilities

Equations

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

def Lean.Lsp.instFromJsonShowDocumentClientCapabilities.fromJson : Json → Except String ShowDocumentClientCapabilities

Equations

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

structure Lean.Lsp.WindowClientCapabilities : Type

• showDocument? : Option ShowDocumentClientCapabilities

def Lean.Lsp.instToJsonWindowClientCapabilities.toJson : WindowClientCapabilities → Json

Equations

• Lean.Lsp.instToJsonWindowClientCapabilities.toJson x✝ = Lean.Json.mkObj [Lean.Json.opt "showDocument" x✝.showDocument?].flatten

instance Lean.Lsp.instToJsonWindowClientCapabilities : ToJson WindowClientCapabilities

Equations

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

instance Lean.Lsp.instFromJsonWindowClientCapabilities : FromJson WindowClientCapabilities

Equations

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

def Lean.Lsp.instFromJsonWindowClientCapabilities.fromJson : Json → Except String WindowClientCapabilities

Equations

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

structure Lean.Lsp.ChangeAnnotationSupport : Type

• groupsOnLabel? : Option Bool

def Lean.Lsp.instToJsonChangeAnnotationSupport.toJson : ChangeAnnotationSupport → Json

Equations

• Lean.Lsp.instToJsonChangeAnnotationSupport.toJson x✝ = Lean.Json.mkObj [Lean.Json.opt "groupsOnLabel" x✝.groupsOnLabel?].flatten

instance Lean.Lsp.instToJsonChangeAnnotationSupport : ToJson ChangeAnnotationSupport

Equations

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

instance Lean.Lsp.instFromJsonChangeAnnotationSupport : FromJson ChangeAnnotationSupport

Equations

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

def Lean.Lsp.instFromJsonChangeAnnotationSupport.fromJson : Json → Except String ChangeAnnotationSupport

Equations

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

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.instToJsonWorkspaceEditClientCapabilities.toJson }

def Lean.Lsp.instToJsonWorkspaceEditClientCapabilities.toJson : WorkspaceEditClientCapabilities → Json

Equations

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

def Lean.Lsp.instFromJsonWorkspaceEditClientCapabilities.fromJson : Json → Except String WorkspaceEditClientCapabilities

Equations

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

instance Lean.Lsp.instFromJsonWorkspaceEditClientCapabilities : FromJson WorkspaceEditClientCapabilities

Equations

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

structure Lean.Lsp.WorkspaceClientCapabilities : Type

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

def Lean.Lsp.instToJsonWorkspaceClientCapabilities.toJson : WorkspaceClientCapabilities → Json

Equations

• Lean.Lsp.instToJsonWorkspaceClientCapabilities.toJson x✝ = Lean.Json.mkObj [Lean.Json.opt "applyEdit" x✝.applyEdit?, Lean.Json.opt "workspaceEdit" x✝.workspaceEdit?].flatten

instance Lean.Lsp.instToJsonWorkspaceClientCapabilities : ToJson WorkspaceClientCapabilities

Equations

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

def Lean.Lsp.instFromJsonWorkspaceClientCapabilities.fromJson : Json → Except String WorkspaceClientCapabilities

Equations

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

instance Lean.Lsp.instFromJsonWorkspaceClientCapabilities : FromJson WorkspaceClientCapabilities

Equations

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

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.

def Lean.Lsp.instToJsonLeanClientCapabilities.toJson : LeanClientCapabilities → Json

Equations

• Lean.Lsp.instToJsonLeanClientCapabilities.toJson x✝ = Lean.Json.mkObj [Lean.Json.opt "silentDiagnosticSupport" x✝.silentDiagnosticSupport?].flatten

instance Lean.Lsp.instToJsonLeanClientCapabilities : ToJson LeanClientCapabilities

Equations

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

instance Lean.Lsp.instFromJsonLeanClientCapabilities : FromJson LeanClientCapabilities

Equations

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

def Lean.Lsp.instFromJsonLeanClientCapabilities.fromJson : Json → Except String LeanClientCapabilities

Equations

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

structure Lean.Lsp.ClientCapabilities : Type

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

  Capabilities for Lean language server extensions.

def Lean.Lsp.instToJsonClientCapabilities.toJson : ClientCapabilities → Json

Equations

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

instance Lean.Lsp.instToJsonClientCapabilities : ToJson ClientCapabilities

Equations

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

def Lean.Lsp.instFromJsonClientCapabilities.fromJson : Json → Except String ClientCapabilities

Equations

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

instance Lean.Lsp.instFromJsonClientCapabilities : FromJson ClientCapabilities

Equations

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

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

Equations

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

structure Lean.Lsp.LeanServerCapabilities : Type

• moduleHierarchyProvider? : Option ModuleHierarchyOptions

instance Lean.Lsp.instFromJsonLeanServerCapabilities : FromJson LeanServerCapabilities

Equations

• Lean.Lsp.instFromJsonLeanServerCapabilities = { fromJson? := Lean.Lsp.instFromJsonLeanServerCapabilities.fromJson }

def Lean.Lsp.instFromJsonLeanServerCapabilities.fromJson : Json → Except String LeanServerCapabilities

Equations

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

instance Lean.Lsp.instToJsonLeanServerCapabilities : ToJson LeanServerCapabilities

Equations

• Lean.Lsp.instToJsonLeanServerCapabilities = { toJson := Lean.Lsp.instToJsonLeanServerCapabilities.toJson }

def Lean.Lsp.instToJsonLeanServerCapabilities.toJson : LeanServerCapabilities → Json

Equations

• Lean.Lsp.instToJsonLeanServerCapabilities.toJson x✝ = Lean.Json.mkObj [Lean.Json.opt "moduleHierarchyProvider" x✝.moduleHierarchyProvider?].flatten

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
• signatureHelpProvider? : Option SignatureHelpOptions
• experimental? : Option LeanServerCapabilities

instance Lean.Lsp.instToJsonServerCapabilities : ToJson ServerCapabilities

Equations

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

def Lean.Lsp.instToJsonServerCapabilities.toJson : ServerCapabilities → Json

Equations

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

def Lean.Lsp.instFromJsonServerCapabilities.fromJson : Json → Except String ServerCapabilities

Equations

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

instance Lean.Lsp.instFromJsonServerCapabilities : FromJson ServerCapabilities

Equations

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