Lapis.Protocol.Capabilities

source

@[reducible, inline]

abbrev Lapis.Protocol.Capabilities.TextDocumentSyncKind :

Type

Equations

Lapis.Protocol.Capabilities.TextDocumentSyncKind = Lapis.Protocol.Generated.TextDocumentSyncKind

Instances For

source

@[reducible, inline]

abbrev Lapis.Protocol.Capabilities.SaveOptions :

Type

Equations

Lapis.Protocol.Capabilities.SaveOptions = Lapis.Protocol.Generated.SaveOptions

Instances For

source

@[reducible, inline]

abbrev Lapis.Protocol.Capabilities.HoverOptions :

Type

Equations

Lapis.Protocol.Capabilities.HoverOptions = Lapis.Protocol.Generated.HoverOptions

Instances For

source

@[reducible, inline]

abbrev Lapis.Protocol.Capabilities.TypeDefinitionOptions :

Type

Equations

Lapis.Protocol.Capabilities.TypeDefinitionOptions = Lapis.Protocol.Generated.TypeDefinitionOptions

Instances For

source

@[reducible, inline]

abbrev Lapis.Protocol.Capabilities.InlayHintOptions :

Type

Equations

Lapis.Protocol.Capabilities.InlayHintOptions = Lapis.Protocol.Generated.InlayHintOptions

Instances For

source

@[reducible, inline]

abbrev Lapis.Protocol.Capabilities.SignatureHelpOptions :

Type

Equations

Lapis.Protocol.Capabilities.SignatureHelpOptions = Lapis.Protocol.Generated.SignatureHelpOptions

Instances For

source

@[reducible, inline]

abbrev Lapis.Protocol.Capabilities.SemanticTokensOptions :

Type

Equations

Lapis.Protocol.Capabilities.SemanticTokensOptions = Lapis.Protocol.Generated.SemanticTokensOptions

Instances For

source

structure Lapis.Protocol.Capabilities.TextDocumentSyncOptions :

Type

Instances For

source

def Lapis.Protocol.Capabilities.instInhabitedTextDocumentSyncOptions.default :

TextDocumentSyncOptions

Equations

Lapis.Protocol.Capabilities.instInhabitedTextDocumentSyncOptions.default = { openClose := default, change := default, save := default }

Instances For

source

@[implicit_reducible]

instance Lapis.Protocol.Capabilities.instInhabitedTextDocumentSyncOptions :

Inhabited TextDocumentSyncOptions

Equations

Lapis.Protocol.Capabilities.instInhabitedTextDocumentSyncOptions = { default := Lapis.Protocol.Capabilities.instInhabitedTextDocumentSyncOptions.default }

source

@[implicit_reducible]

instance Lapis.Protocol.Capabilities.instToJsonTextDocumentSyncOptions :

Lean.ToJson TextDocumentSyncOptions

Equations

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

source

@[implicit_reducible]

instance Lapis.Protocol.Capabilities.instFromJsonTextDocumentSyncOptions :

Lean.FromJson TextDocumentSyncOptions

Equations

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

source

structure Lapis.Protocol.Capabilities.CompletionOptions :

Type

triggerCharacters : Option (Array String)
resolveProvider : Option Bool

Instances For

source

def Lapis.Protocol.Capabilities.instInhabitedCompletionOptions.default :

CompletionOptions

Equations

Lapis.Protocol.Capabilities.instInhabitedCompletionOptions.default = { triggerCharacters := default, resolveProvider := default }

Instances For

source

@[implicit_reducible]

instance Lapis.Protocol.Capabilities.instInhabitedCompletionOptions :

Inhabited CompletionOptions

Equations

Lapis.Protocol.Capabilities.instInhabitedCompletionOptions = { default := Lapis.Protocol.Capabilities.instInhabitedCompletionOptions.default }

source

def Lapis.Protocol.Capabilities.instReprCompletionOptions.repr :

CompletionOptions → Nat → Std.Format

Equations

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

Instances For

source

@[implicit_reducible]

instance Lapis.Protocol.Capabilities.instReprCompletionOptions :

Repr CompletionOptions

Equations

Lapis.Protocol.Capabilities.instReprCompletionOptions = { reprPrec := Lapis.Protocol.Capabilities.instReprCompletionOptions.repr }

source

@[implicit_reducible]

instance Lapis.Protocol.Capabilities.instToJsonCompletionOptions :

Lean.ToJson CompletionOptions

Equations

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

source

@[implicit_reducible]

instance Lapis.Protocol.Capabilities.instFromJsonCompletionOptions :

Lean.FromJson CompletionOptions

Equations

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

source

structure Lapis.Protocol.Capabilities.ServerCapabilities :

Type

textDocumentSync : Option TextDocumentSyncOptions
completionProvider : Option CompletionOptions
hoverProvider : Option Bool
signatureHelpProvider : Option SignatureHelpOptions
definitionProvider : Option Bool
typeDefinitionProvider : Option TypeDefinitionOptions
referencesProvider : Option Bool
documentSymbolProvider : Option Bool
workspaceSymbolProvider : Option Bool
codeActionProvider : Option Bool
documentFormattingProvider : Option Bool
renameProvider : Option Bool
inlayHintProvider : Option InlayHintOptions
semanticTokensProvider : Option SemanticTokensOptions

Instances For

source

@[implicit_reducible]

instance Lapis.Protocol.Capabilities.instInhabitedServerCapabilities :

Inhabited ServerCapabilities

Equations

Lapis.Protocol.Capabilities.instInhabitedServerCapabilities = { default := Lapis.Protocol.Capabilities.instInhabitedServerCapabilities.default }

source

def Lapis.Protocol.Capabilities.instInhabitedServerCapabilities.default :

ServerCapabilities

Equations

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

Instances For

source

@[implicit_reducible]

instance Lapis.Protocol.Capabilities.instToJsonServerCapabilities :

Lean.ToJson ServerCapabilities

Equations

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

source

@[implicit_reducible]

instance Lapis.Protocol.Capabilities.instFromJsonServerCapabilities :

Lean.FromJson ServerCapabilities

Equations

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

source

structure Lapis.Protocol.Capabilities.ClientCapabilities :

Type

TODO: Client capabilities

Instances For

source

def Lapis.Protocol.Capabilities.instInhabitedClientCapabilities.default :

ClientCapabilities

Equations

Lapis.Protocol.Capabilities.instInhabitedClientCapabilities.default = { }

Instances For

source

@[implicit_reducible]

instance Lapis.Protocol.Capabilities.instInhabitedClientCapabilities :

Inhabited ClientCapabilities

Equations

Lapis.Protocol.Capabilities.instInhabitedClientCapabilities = { default := Lapis.Protocol.Capabilities.instInhabitedClientCapabilities.default }

source

def Lapis.Protocol.Capabilities.instReprClientCapabilities.repr :

ClientCapabilities → Nat → Std.Format

Equations

Lapis.Protocol.Capabilities.instReprClientCapabilities.repr x✝ prec✝ = Std.Format.bracket "{ " Std.Format.nil " }"

Instances For

source

@[implicit_reducible]

instance Lapis.Protocol.Capabilities.instReprClientCapabilities :

Repr ClientCapabilities

Equations

Lapis.Protocol.Capabilities.instReprClientCapabilities = { reprPrec := Lapis.Protocol.Capabilities.instReprClientCapabilities.repr }

source

@[implicit_reducible]

instance Lapis.Protocol.Capabilities.instToJsonClientCapabilities :

Lean.ToJson ClientCapabilities

Equations

Lapis.Protocol.Capabilities.instToJsonClientCapabilities = { toJson := fun (x : Lapis.Protocol.Capabilities.ClientCapabilities) => Lean.Json.mkObj [] }

source

@[implicit_reducible]

instance Lapis.Protocol.Capabilities.instFromJsonClientCapabilities :

Lean.FromJson ClientCapabilities

Equations

Lapis.Protocol.Capabilities.instFromJsonClientCapabilities = { fromJson? := fun (x : Lean.Json) => pure { } }