structure Lean.Lsp.CompletionOptions : Type

• triggerCharacters? : Option (Array String)
• allCommitCharacters? : Option (Array String)
• resolveProvider : Bool

instance Lean.Lsp.instFromJsonCompletionOptions : Lean.FromJson Lean.Lsp.CompletionOptions

instance Lean.Lsp.instToJsonCompletionOptions : Lean.ToJson Lean.Lsp.CompletionOptions

inductive Lean.Lsp.CompletionItemKind : Type

• text: Lean.Lsp.CompletionItemKind
• method: Lean.Lsp.CompletionItemKind
• function: Lean.Lsp.CompletionItemKind
• constructor: Lean.Lsp.CompletionItemKind
• field: Lean.Lsp.CompletionItemKind
• variable: Lean.Lsp.CompletionItemKind
• class: Lean.Lsp.CompletionItemKind
• interface: Lean.Lsp.CompletionItemKind
• module: Lean.Lsp.CompletionItemKind
• property: Lean.Lsp.CompletionItemKind
• unit: Lean.Lsp.CompletionItemKind
• value: Lean.Lsp.CompletionItemKind
• enum: Lean.Lsp.CompletionItemKind
• keyword: Lean.Lsp.CompletionItemKind
• snippet: Lean.Lsp.CompletionItemKind
• color: Lean.Lsp.CompletionItemKind
• file: Lean.Lsp.CompletionItemKind
• reference: Lean.Lsp.CompletionItemKind
• folder: Lean.Lsp.CompletionItemKind
• enumMember: Lean.Lsp.CompletionItemKind
• constant: Lean.Lsp.CompletionItemKind
• struct: Lean.Lsp.CompletionItemKind
• event: Lean.Lsp.CompletionItemKind
• operator: Lean.Lsp.CompletionItemKind
• typeParameter: Lean.Lsp.CompletionItemKind

instance Lean.Lsp.instInhabitedCompletionItemKind : Inhabited Lean.Lsp.CompletionItemKind

instance Lean.Lsp.instDecidableEqCompletionItemKind : DecidableEq Lean.Lsp.CompletionItemKind

instance Lean.Lsp.instReprCompletionItemKind : Repr Lean.Lsp.CompletionItemKind

instance Lean.Lsp.instToJsonCompletionItemKind : Lean.ToJson Lean.Lsp.CompletionItemKind

instance Lean.Lsp.instFromJsonCompletionItemKind : Lean.FromJson Lean.Lsp.CompletionItemKind

structure Lean.Lsp.InsertReplaceEdit : Type

• newText : String
• insert : Lean.Lsp.Range
• replace : Lean.Lsp.Range

instance Lean.Lsp.instFromJsonInsertReplaceEdit : Lean.FromJson Lean.Lsp.InsertReplaceEdit

instance Lean.Lsp.instToJsonInsertReplaceEdit : Lean.ToJson Lean.Lsp.InsertReplaceEdit

structure Lean.Lsp.CompletionItem : Type

• label : String
• detail? : Option String
• documentation? : Option Lean.Lsp.MarkupContent
• kind? : Option Lean.Lsp.CompletionItemKind
• textEdit? : Option Lean.Lsp.InsertReplaceEdit

instance Lean.Lsp.instFromJsonCompletionItem : Lean.FromJson Lean.Lsp.CompletionItem

instance Lean.Lsp.instToJsonCompletionItem : Lean.ToJson Lean.Lsp.CompletionItem

instance Lean.Lsp.instInhabitedCompletionItem : Inhabited Lean.Lsp.CompletionItem

structure Lean.Lsp.CompletionList : Type

• isIncomplete : Bool
• items : Array Lean.Lsp.CompletionItem

instance Lean.Lsp.instFromJsonCompletionList : Lean.FromJson Lean.Lsp.CompletionList

instance Lean.Lsp.instToJsonCompletionList : Lean.ToJson Lean.Lsp.CompletionList

structure Lean.Lsp.CompletionParamsextends Lean.Lsp.TextDocumentPositionParams : Type

instance Lean.Lsp.instFromJsonCompletionParams : Lean.FromJson Lean.Lsp.CompletionParams

instance Lean.Lsp.instToJsonCompletionParams : Lean.ToJson Lean.Lsp.CompletionParams

structure Lean.Lsp.Hover : Type

• contents : Lean.Lsp.MarkupContent
• range? : Option Lean.Lsp.Range

instance Lean.Lsp.instToJsonHover : Lean.ToJson Lean.Lsp.Hover

instance Lean.Lsp.instFromJsonHover : Lean.FromJson Lean.Lsp.Hover

structure Lean.Lsp.HoverParamsextends Lean.Lsp.TextDocumentPositionParams : Type

instance Lean.Lsp.instFromJsonHoverParams : Lean.FromJson Lean.Lsp.HoverParams

instance Lean.Lsp.instToJsonHoverParams : Lean.ToJson Lean.Lsp.HoverParams

structure Lean.Lsp.DeclarationParamsextends Lean.Lsp.TextDocumentPositionParams : Type

instance Lean.Lsp.instFromJsonDeclarationParams : Lean.FromJson Lean.Lsp.DeclarationParams

instance Lean.Lsp.instToJsonDeclarationParams : Lean.ToJson Lean.Lsp.DeclarationParams

structure Lean.Lsp.DefinitionParamsextends Lean.Lsp.TextDocumentPositionParams : Type

instance Lean.Lsp.instFromJsonDefinitionParams : Lean.FromJson Lean.Lsp.DefinitionParams

instance Lean.Lsp.instToJsonDefinitionParams : Lean.ToJson Lean.Lsp.DefinitionParams

structure Lean.Lsp.TypeDefinitionParamsextends Lean.Lsp.TextDocumentPositionParams : Type

instance Lean.Lsp.instFromJsonTypeDefinitionParams : Lean.FromJson Lean.Lsp.TypeDefinitionParams

instance Lean.Lsp.instToJsonTypeDefinitionParams : Lean.ToJson Lean.Lsp.TypeDefinitionParams

structure Lean.Lsp.ReferenceContext : Type

• includeDeclaration : Bool

instance Lean.Lsp.instFromJsonReferenceContext : Lean.FromJson Lean.Lsp.ReferenceContext

instance Lean.Lsp.instToJsonReferenceContext : Lean.ToJson Lean.Lsp.ReferenceContext

structure Lean.Lsp.ReferenceParamsextends Lean.Lsp.TextDocumentPositionParams : Type

• textDocument : Lean.Lsp.TextDocumentIdentifier
• position : Lean.Lsp.Position
• context : Lean.Lsp.ReferenceContext

instance Lean.Lsp.instFromJsonReferenceParams : Lean.FromJson Lean.Lsp.ReferenceParams

instance Lean.Lsp.instToJsonReferenceParams : Lean.ToJson Lean.Lsp.ReferenceParams

structure Lean.Lsp.WorkspaceSymbolParams : Type

• query : String

instance Lean.Lsp.instFromJsonWorkspaceSymbolParams : Lean.FromJson Lean.Lsp.WorkspaceSymbolParams

instance Lean.Lsp.instToJsonWorkspaceSymbolParams : Lean.ToJson Lean.Lsp.WorkspaceSymbolParams

structure Lean.Lsp.DocumentHighlightParamsextends Lean.Lsp.TextDocumentPositionParams : Type

instance Lean.Lsp.instFromJsonDocumentHighlightParams : Lean.FromJson Lean.Lsp.DocumentHighlightParams

instance Lean.Lsp.instToJsonDocumentHighlightParams : Lean.ToJson Lean.Lsp.DocumentHighlightParams

inductive Lean.Lsp.DocumentHighlightKind : Type

• text: Lean.Lsp.DocumentHighlightKind
• read: Lean.Lsp.DocumentHighlightKind
• write: Lean.Lsp.DocumentHighlightKind

instance Lean.Lsp.instToJsonDocumentHighlightKind : Lean.ToJson Lean.Lsp.DocumentHighlightKind

structure Lean.Lsp.DocumentHighlight : Type

• range : Lean.Lsp.Range
• kind? : Option Lean.Lsp.DocumentHighlightKind

instance Lean.Lsp.instToJsonDocumentHighlight : Lean.ToJson Lean.Lsp.DocumentHighlight

@[inline, reducible]

abbrev Lean.Lsp.DocumentHighlightResult : Type

structure Lean.Lsp.DocumentSymbolParams : Type

• textDocument : Lean.Lsp.TextDocumentIdentifier

instance Lean.Lsp.instFromJsonDocumentSymbolParams : Lean.FromJson Lean.Lsp.DocumentSymbolParams

instance Lean.Lsp.instToJsonDocumentSymbolParams : Lean.ToJson Lean.Lsp.DocumentSymbolParams

inductive Lean.Lsp.SymbolKind : Type

• file: Lean.Lsp.SymbolKind
• module: Lean.Lsp.SymbolKind
• namespace: Lean.Lsp.SymbolKind
• package: Lean.Lsp.SymbolKind
• class: Lean.Lsp.SymbolKind
• method: Lean.Lsp.SymbolKind
• property: Lean.Lsp.SymbolKind
• field: Lean.Lsp.SymbolKind
• constructor: Lean.Lsp.SymbolKind
• enum: Lean.Lsp.SymbolKind
• interface: Lean.Lsp.SymbolKind
• function: Lean.Lsp.SymbolKind
• variable: Lean.Lsp.SymbolKind
• constant: Lean.Lsp.SymbolKind
• string: Lean.Lsp.SymbolKind
• number: Lean.Lsp.SymbolKind
• boolean: Lean.Lsp.SymbolKind
• array: Lean.Lsp.SymbolKind
• object: Lean.Lsp.SymbolKind
• key: Lean.Lsp.SymbolKind
• null: Lean.Lsp.SymbolKind
• enumMember: Lean.Lsp.SymbolKind
• struct: Lean.Lsp.SymbolKind
• event: Lean.Lsp.SymbolKind
• operator: Lean.Lsp.SymbolKind
• typeParameter: Lean.Lsp.SymbolKind

instance Lean.Lsp.instToJsonSymbolKind : Lean.ToJson Lean.Lsp.SymbolKind

structure Lean.Lsp.DocumentSymbolAux (Self : Type) : Type

• name : String
• detail? : Option String
• kind : Lean.Lsp.SymbolKind
• range : Lean.Lsp.Range
• selectionRange : Lean.Lsp.Range
• children? : Option (Array Self)

instance Lean.Lsp.instToJsonDocumentSymbolAux : {Self : Type} → [inst : Lean.ToJson Self] → Lean.ToJson (Lean.Lsp.DocumentSymbolAux Self)

inductive Lean.Lsp.DocumentSymbol : Type

• mk: Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol → Lean.Lsp.DocumentSymbol

instance Lean.Lsp.instToJsonDocumentSymbol : Lean.ToJson Lean.Lsp.DocumentSymbol

partial def Lean.Lsp.instToJsonDocumentSymbol.go : Lean.Lsp.DocumentSymbol → Lean.Json

structure Lean.Lsp.DocumentSymbolResult : Type

• syms : Array Lean.Lsp.DocumentSymbol

instance Lean.Lsp.instToJsonDocumentSymbolResult : Lean.ToJson Lean.Lsp.DocumentSymbolResult

inductive Lean.Lsp.SymbolTag : Type

• deprecated: Lean.Lsp.SymbolTag

instance Lean.Lsp.instToJsonSymbolTag : Lean.ToJson Lean.Lsp.SymbolTag

structure Lean.Lsp.SymbolInformation : Type

• name : String
• kind : Lean.Lsp.SymbolKind
• tags : Array Lean.Lsp.SymbolTag
• location : Lean.Lsp.Location
• containerName? : Option String

instance Lean.Lsp.instToJsonSymbolInformation : Lean.ToJson Lean.Lsp.SymbolInformation

inductive Lean.Lsp.SemanticTokenType : Type

• keyword: Lean.Lsp.SemanticTokenType
• variable: Lean.Lsp.SemanticTokenType
• property: Lean.Lsp.SemanticTokenType
• function: Lean.Lsp.SemanticTokenType
• namespace: Lean.Lsp.SemanticTokenType
• type: Lean.Lsp.SemanticTokenType
• class: Lean.Lsp.SemanticTokenType
• enum: Lean.Lsp.SemanticTokenType
• interface: Lean.Lsp.SemanticTokenType
• struct: Lean.Lsp.SemanticTokenType
• typeParameter: Lean.Lsp.SemanticTokenType
• parameter: Lean.Lsp.SemanticTokenType
• enumMember: Lean.Lsp.SemanticTokenType
• event: Lean.Lsp.SemanticTokenType
• method: Lean.Lsp.SemanticTokenType
• macro: Lean.Lsp.SemanticTokenType
• modifier: Lean.Lsp.SemanticTokenType
• comment: Lean.Lsp.SemanticTokenType
• string: Lean.Lsp.SemanticTokenType
• number: Lean.Lsp.SemanticTokenType
• regexp: Lean.Lsp.SemanticTokenType
• operator: Lean.Lsp.SemanticTokenType
• decorator: Lean.Lsp.SemanticTokenType
• leanSorryLike: Lean.Lsp.SemanticTokenType

instance Lean.Lsp.instToJsonSemanticTokenType : Lean.ToJson Lean.Lsp.SemanticTokenType

instance Lean.Lsp.instFromJsonSemanticTokenType : Lean.FromJson Lean.Lsp.SemanticTokenType

def Lean.Lsp.SemanticTokenType.names : Array String

def Lean.Lsp.SemanticTokenType.toNat (type : Lean.Lsp.SemanticTokenType) : Nat

inductive Lean.Lsp.SemanticTokenModifier : Type

• declaration: Lean.Lsp.SemanticTokenModifier
• definition: Lean.Lsp.SemanticTokenModifier
• readonly: Lean.Lsp.SemanticTokenModifier
• static: Lean.Lsp.SemanticTokenModifier
• deprecated: Lean.Lsp.SemanticTokenModifier
• abstract: Lean.Lsp.SemanticTokenModifier
• async: Lean.Lsp.SemanticTokenModifier
• modification: Lean.Lsp.SemanticTokenModifier
• documentation: Lean.Lsp.SemanticTokenModifier
• defaultLibrary: Lean.Lsp.SemanticTokenModifier

The semantic token modifiers included by default in the LSP specification. Not used by the Lean core, but implementing them here allows them to be utilized by users extending the Lean server.

instance Lean.Lsp.instToJsonSemanticTokenModifier : Lean.ToJson Lean.Lsp.SemanticTokenModifier

instance Lean.Lsp.instFromJsonSemanticTokenModifier : Lean.FromJson Lean.Lsp.SemanticTokenModifier

def Lean.Lsp.SemanticTokenModifier.names : Array String

def Lean.Lsp.SemanticTokenModifier.toNat (modifier : Lean.Lsp.SemanticTokenModifier) : Nat

structure Lean.Lsp.SemanticTokensLegend : Type

• tokenTypes : Array String
• tokenModifiers : Array String

instance Lean.Lsp.instFromJsonSemanticTokensLegend : Lean.FromJson Lean.Lsp.SemanticTokensLegend

instance Lean.Lsp.instToJsonSemanticTokensLegend : Lean.ToJson Lean.Lsp.SemanticTokensLegend

structure Lean.Lsp.SemanticTokensOptions : Type

• legend : Lean.Lsp.SemanticTokensLegend
• range : Bool
• full : Bool

instance Lean.Lsp.instFromJsonSemanticTokensOptions : Lean.FromJson Lean.Lsp.SemanticTokensOptions

instance Lean.Lsp.instToJsonSemanticTokensOptions : Lean.ToJson Lean.Lsp.SemanticTokensOptions

structure Lean.Lsp.SemanticTokensParams : Type

• textDocument : Lean.Lsp.TextDocumentIdentifier

instance Lean.Lsp.instFromJsonSemanticTokensParams : Lean.FromJson Lean.Lsp.SemanticTokensParams

instance Lean.Lsp.instToJsonSemanticTokensParams : Lean.ToJson Lean.Lsp.SemanticTokensParams

structure Lean.Lsp.SemanticTokensRangeParams : Type

• textDocument : Lean.Lsp.TextDocumentIdentifier
• range : Lean.Lsp.Range

instance Lean.Lsp.instFromJsonSemanticTokensRangeParams : Lean.FromJson Lean.Lsp.SemanticTokensRangeParams

instance Lean.Lsp.instToJsonSemanticTokensRangeParams : Lean.ToJson Lean.Lsp.SemanticTokensRangeParams

structure Lean.Lsp.SemanticTokens : Type

• resultId? : Option String
• data : Array Nat

instance Lean.Lsp.instFromJsonSemanticTokens : Lean.FromJson Lean.Lsp.SemanticTokens

instance Lean.Lsp.instToJsonSemanticTokens : Lean.ToJson Lean.Lsp.SemanticTokens

structure Lean.Lsp.FoldingRangeParams : Type

• textDocument : Lean.Lsp.TextDocumentIdentifier

instance Lean.Lsp.instFromJsonFoldingRangeParams : Lean.FromJson Lean.Lsp.FoldingRangeParams

instance Lean.Lsp.instToJsonFoldingRangeParams : Lean.ToJson Lean.Lsp.FoldingRangeParams

inductive Lean.Lsp.FoldingRangeKind : Type

• comment: Lean.Lsp.FoldingRangeKind
• imports: Lean.Lsp.FoldingRangeKind
• region: Lean.Lsp.FoldingRangeKind

instance Lean.Lsp.instToJsonFoldingRangeKind : Lean.ToJson Lean.Lsp.FoldingRangeKind

structure Lean.Lsp.FoldingRange : Type

• startLine : Nat
• endLine : Nat
• kind? : Option Lean.Lsp.FoldingRangeKind

instance Lean.Lsp.instToJsonFoldingRange : Lean.ToJson Lean.Lsp.FoldingRange