Lapis.Protocol.Capabilities

source

inductive Lapis.Protocol.Capabilities.TextDocumentSyncKind :

Type

How documents are synced to the server

Instances For

source

def Lapis.Protocol.Capabilities.instInhabitedTextDocumentSyncKind.default :

TextDocumentSyncKind

Equations

Lapis.Protocol.Capabilities.instInhabitedTextDocumentSyncKind.default = Lapis.Protocol.Capabilities.TextDocumentSyncKind.none

Instances For

source

instance Lapis.Protocol.Capabilities.instInhabitedTextDocumentSyncKind :

Inhabited TextDocumentSyncKind

Equations

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

source

instance Lapis.Protocol.Capabilities.instBEqTextDocumentSyncKind :

BEq TextDocumentSyncKind

Equations

Lapis.Protocol.Capabilities.instBEqTextDocumentSyncKind = { beq := Lapis.Protocol.Capabilities.instBEqTextDocumentSyncKind.beq }

source

def Lapis.Protocol.Capabilities.instBEqTextDocumentSyncKind.beq :

TextDocumentSyncKind → TextDocumentSyncKind → Bool

Equations

Lapis.Protocol.Capabilities.instBEqTextDocumentSyncKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Lapis.Protocol.Capabilities.instReprTextDocumentSyncKind :

Repr TextDocumentSyncKind

Equations

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

source

def Lapis.Protocol.Capabilities.instReprTextDocumentSyncKind.repr :

TextDocumentSyncKind → Nat → Std.Format

Equations

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

Instances For

source

instance Lapis.Protocol.Capabilities.instToJsonTextDocumentSyncKind :

Lean.ToJson TextDocumentSyncKind

Equations

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

source

instance Lapis.Protocol.Capabilities.instFromJsonTextDocumentSyncKind :

Lean.FromJson TextDocumentSyncKind

Equations

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

source

structure Lapis.Protocol.Capabilities.SaveOptions :

Type

includeText : Option Bool

Instances For

source

instance Lapis.Protocol.Capabilities.instInhabitedSaveOptions :

Inhabited SaveOptions

Equations

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

source

def Lapis.Protocol.Capabilities.instInhabitedSaveOptions.default :

SaveOptions

Equations

Lapis.Protocol.Capabilities.instInhabitedSaveOptions.default = { includeText := default }

Instances For

source

instance Lapis.Protocol.Capabilities.instReprSaveOptions :

Repr SaveOptions

Equations

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

source

def Lapis.Protocol.Capabilities.instReprSaveOptions.repr :

SaveOptions → Nat → Std.Format

Equations

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

Instances For

source

instance Lapis.Protocol.Capabilities.instToJsonSaveOptions :

Lean.ToJson SaveOptions

Equations

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

source

instance Lapis.Protocol.Capabilities.instFromJsonSaveOptions :

Lean.FromJson SaveOptions

Equations

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

source

structure Lapis.Protocol.Capabilities.TextDocumentSyncOptions :

Type

Instances For

source

instance Lapis.Protocol.Capabilities.instInhabitedTextDocumentSyncOptions :

Inhabited TextDocumentSyncOptions

Equations

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

source

def Lapis.Protocol.Capabilities.instInhabitedTextDocumentSyncOptions.default :

TextDocumentSyncOptions

Equations

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

Instances For

source

instance Lapis.Protocol.Capabilities.instReprTextDocumentSyncOptions :

Repr TextDocumentSyncOptions

Equations

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

source

def Lapis.Protocol.Capabilities.instReprTextDocumentSyncOptions.repr :

TextDocumentSyncOptions → Nat → Std.Format

Equations

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

Instances For

source

instance Lapis.Protocol.Capabilities.instToJsonTextDocumentSyncOptions :

Lean.ToJson TextDocumentSyncOptions

Equations

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

source

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

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

instance Lapis.Protocol.Capabilities.instReprCompletionOptions :

Repr CompletionOptions

Equations

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

source

instance Lapis.Protocol.Capabilities.instToJsonCompletionOptions :

Lean.ToJson CompletionOptions

Equations

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

source

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.HoverOptions :

Type

workDoneProgress : Option Bool

Instances For

source

def Lapis.Protocol.Capabilities.instInhabitedHoverOptions.default :

HoverOptions

Equations

Lapis.Protocol.Capabilities.instInhabitedHoverOptions.default = { workDoneProgress := default }

Instances For

source

instance Lapis.Protocol.Capabilities.instInhabitedHoverOptions :

Inhabited HoverOptions

Equations

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

source

instance Lapis.Protocol.Capabilities.instReprHoverOptions :

Repr HoverOptions

Equations

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

source

def Lapis.Protocol.Capabilities.instReprHoverOptions.repr :

HoverOptions → Nat → Std.Format

Equations

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

Instances For

source

instance Lapis.Protocol.Capabilities.instToJsonHoverOptions :

Lean.ToJson HoverOptions

Equations

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

source

instance Lapis.Protocol.Capabilities.instFromJsonHoverOptions :

Lean.FromJson HoverOptions

Equations

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

source

structure Lapis.Protocol.Capabilities.TypeDefinitionOptions :

Type

workDoneProgress : Option Bool

Instances For

source

def Lapis.Protocol.Capabilities.instInhabitedTypeDefinitionOptions.default :

TypeDefinitionOptions

Equations

Lapis.Protocol.Capabilities.instInhabitedTypeDefinitionOptions.default = { workDoneProgress := default }

Instances For

source

instance Lapis.Protocol.Capabilities.instInhabitedTypeDefinitionOptions :

Inhabited TypeDefinitionOptions

Equations

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

source

def Lapis.Protocol.Capabilities.instReprTypeDefinitionOptions.repr :

TypeDefinitionOptions → Nat → Std.Format

Equations

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

Instances For

source

instance Lapis.Protocol.Capabilities.instReprTypeDefinitionOptions :

Repr TypeDefinitionOptions

Equations

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

source

instance Lapis.Protocol.Capabilities.instToJsonTypeDefinitionOptions :

Lean.ToJson TypeDefinitionOptions

Equations

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

source

instance Lapis.Protocol.Capabilities.instFromJsonTypeDefinitionOptions :

Lean.FromJson TypeDefinitionOptions

Equations

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

source

structure Lapis.Protocol.Capabilities.InlayHintOptions :

Type

workDoneProgress : Option Bool
resolveProvider : Option Bool

Instances For

source

def Lapis.Protocol.Capabilities.instInhabitedInlayHintOptions.default :

InlayHintOptions

Equations

Lapis.Protocol.Capabilities.instInhabitedInlayHintOptions.default = { workDoneProgress := default, resolveProvider := default }

Instances For

source

instance Lapis.Protocol.Capabilities.instInhabitedInlayHintOptions :

Inhabited InlayHintOptions

Equations

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

source

instance Lapis.Protocol.Capabilities.instReprInlayHintOptions :

Repr InlayHintOptions

Equations

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

source

def Lapis.Protocol.Capabilities.instReprInlayHintOptions.repr :

InlayHintOptions → Nat → Std.Format

Equations

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

Instances For

source

instance Lapis.Protocol.Capabilities.instToJsonInlayHintOptions :

Lean.ToJson InlayHintOptions

Equations

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

source

instance Lapis.Protocol.Capabilities.instFromJsonInlayHintOptions :

Lean.FromJson InlayHintOptions

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
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 Generated.SemanticTokensOptions

Instances For

source

def Lapis.Protocol.Capabilities.instInhabitedServerCapabilities.default :

ServerCapabilities

Equations

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

Instances For

source

instance Lapis.Protocol.Capabilities.instInhabitedServerCapabilities :

Inhabited ServerCapabilities

Equations

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

source

instance Lapis.Protocol.Capabilities.instToJsonServerCapabilities :

Lean.ToJson ServerCapabilities

Equations

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

source

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

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

instance Lapis.Protocol.Capabilities.instReprClientCapabilities :

Repr ClientCapabilities

Equations

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

source

instance Lapis.Protocol.Capabilities.instToJsonClientCapabilities :

Lean.ToJson ClientCapabilities

Equations

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

source

instance Lapis.Protocol.Capabilities.instFromJsonClientCapabilities :

Lean.FromJson ClientCapabilities

Equations

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