structure Lean.Lsp.CompletionOptions : Type

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

instance Lean.Lsp.instFromJsonCompletionOptions : FromJson CompletionOptions

def Lean.Lsp.instFromJsonCompletionOptions.fromJson : Json → Except String CompletionOptions

instance Lean.Lsp.instToJsonCompletionOptions : ToJson CompletionOptions

def Lean.Lsp.instToJsonCompletionOptions.toJson : CompletionOptions → Json

inductive Lean.Lsp.CompletionItemKind : Type

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

def Lean.Lsp.instInhabitedCompletionItemKind.default : CompletionItemKind

instance Lean.Lsp.instInhabitedCompletionItemKind : Inhabited CompletionItemKind

instance Lean.Lsp.instDecidableEqCompletionItemKind : DecidableEq CompletionItemKind

def Lean.Lsp.instReprCompletionItemKind.repr : CompletionItemKind → Nat → Format

instance Lean.Lsp.instReprCompletionItemKind : Repr CompletionItemKind

instance Lean.Lsp.instHashableCompletionItemKind : Hashable CompletionItemKind

def Lean.Lsp.instHashableCompletionItemKind.hash : CompletionItemKind → UInt64

instance Lean.Lsp.instToJsonCompletionItemKind : ToJson CompletionItemKind

instance Lean.Lsp.instFromJsonCompletionItemKind : FromJson CompletionItemKind

structure Lean.Lsp.InsertReplaceEdit : Type

• newText : String
• insert : Range
• replace : Range

def Lean.Lsp.instFromJsonInsertReplaceEdit.fromJson : Json → Except String InsertReplaceEdit

instance Lean.Lsp.instFromJsonInsertReplaceEdit : FromJson InsertReplaceEdit

instance Lean.Lsp.instToJsonInsertReplaceEdit : ToJson InsertReplaceEdit

def Lean.Lsp.instToJsonInsertReplaceEdit.toJson : InsertReplaceEdit → Json

def Lean.Lsp.instBEqInsertReplaceEdit.beq : InsertReplaceEdit → InsertReplaceEdit → Bool

instance Lean.Lsp.instBEqInsertReplaceEdit : BEq InsertReplaceEdit

def Lean.Lsp.instHashableInsertReplaceEdit.hash : InsertReplaceEdit → UInt64

instance Lean.Lsp.instHashableInsertReplaceEdit : Hashable InsertReplaceEdit

inductive Lean.Lsp.CompletionItemTag : Type

• deprecated : CompletionItemTag

def Lean.Lsp.instInhabitedCompletionItemTag.default : CompletionItemTag

instance Lean.Lsp.instInhabitedCompletionItemTag : Inhabited CompletionItemTag

instance Lean.Lsp.instDecidableEqCompletionItemTag : DecidableEq CompletionItemTag

def Lean.Lsp.instReprCompletionItemTag.repr : CompletionItemTag → Nat → Format

instance Lean.Lsp.instReprCompletionItemTag : Repr CompletionItemTag

instance Lean.Lsp.instHashableCompletionItemTag : Hashable CompletionItemTag

def Lean.Lsp.instHashableCompletionItemTag.hash : CompletionItemTag → UInt64

instance Lean.Lsp.instToJsonCompletionItemTag : ToJson CompletionItemTag

instance Lean.Lsp.instFromJsonCompletionItemTag : FromJson CompletionItemTag

structure Lean.Lsp.CompletionItem : Type

• label : String
• detail? : Option String
• documentation? : Option MarkupContent
• kind? : Option CompletionItemKind
• textEdit? : Option InsertReplaceEdit
• sortText? : Option String
• data? : Option Json
• tags? : Option (Array CompletionItemTag)

def Lean.Lsp.instFromJsonCompletionItem.fromJson : Json → Except String CompletionItem

instance Lean.Lsp.instFromJsonCompletionItem : FromJson CompletionItem

instance Lean.Lsp.instToJsonCompletionItem : ToJson CompletionItem

def Lean.Lsp.instToJsonCompletionItem.toJson : CompletionItem → Json

instance Lean.Lsp.instInhabitedCompletionItem : Inhabited CompletionItem

def Lean.Lsp.instInhabitedCompletionItem.default : CompletionItem

instance Lean.Lsp.instBEqCompletionItem : BEq CompletionItem

def Lean.Lsp.instBEqCompletionItem.beq : CompletionItem → CompletionItem → Bool

instance Lean.Lsp.instHashableCompletionItem : Hashable CompletionItem

def Lean.Lsp.instHashableCompletionItem.hash : CompletionItem → UInt64

structure Lean.Lsp.CompletionList : Type

• isIncomplete : Bool
• items : Array CompletionItem

instance Lean.Lsp.instFromJsonCompletionList : FromJson CompletionList

def Lean.Lsp.instFromJsonCompletionList.fromJson : Json → Except String CompletionList

instance Lean.Lsp.instToJsonCompletionList : ToJson CompletionList

def Lean.Lsp.instToJsonCompletionList.toJson : CompletionList → Json

inductive Lean.Lsp.CompletionIdentifier : Type

Identifier that is sent from the server to the client as part of the CompletionItem.data? field. Needed to resolve the CompletionItem when the client sends a completionItem/resolve request for that item, again containing the data? field provided by the server.

• const (declName : Name) : CompletionIdentifier
• fvar (id : FVarId) : CompletionIdentifier

instance Lean.Lsp.instBEqCompletionIdentifier : BEq CompletionIdentifier

def Lean.Lsp.instBEqCompletionIdentifier.beq : CompletionIdentifier → CompletionIdentifier → Bool

instance Lean.Lsp.instHashableCompletionIdentifier : Hashable CompletionIdentifier

def Lean.Lsp.instHashableCompletionIdentifier.hash : CompletionIdentifier → UInt64

instance Lean.Lsp.instToJsonCompletionIdentifier : ToJson CompletionIdentifier

instance Lean.Lsp.instFromJsonCompletionIdentifier : FromJson CompletionIdentifier

structure Lean.Lsp.ResolvableCompletionItemData : Type

• mod : Name
• pos : Position
• cPos? : Option Nat

  Position of the completion info that this completion item was created from.

• id? : Option CompletionIdentifier

instance Lean.Lsp.instBEqResolvableCompletionItemData : BEq ResolvableCompletionItemData

def Lean.Lsp.instBEqResolvableCompletionItemData.beq : ResolvableCompletionItemData → ResolvableCompletionItemData → Bool

def Lean.Lsp.instHashableResolvableCompletionItemData.hash : ResolvableCompletionItemData → UInt64

instance Lean.Lsp.instHashableResolvableCompletionItemData : Hashable ResolvableCompletionItemData

instance Lean.Lsp.instToJsonResolvableCompletionItemData : ToJson ResolvableCompletionItemData

instance Lean.Lsp.instFromJsonResolvableCompletionItemData : FromJson ResolvableCompletionItemData

structure Lean.Lsp.ResolvableCompletionItem : Type

• label : String
• detail? : Option String
• documentation? : Option MarkupContent
• kind? : Option CompletionItemKind
• textEdit? : Option InsertReplaceEdit
• sortText? : Option String
• data? : Option ResolvableCompletionItemData
• tags? : Option (Array CompletionItemTag)

def Lean.Lsp.instFromJsonResolvableCompletionItem.fromJson : Json → Except String ResolvableCompletionItem

instance Lean.Lsp.instFromJsonResolvableCompletionItem : FromJson ResolvableCompletionItem

instance Lean.Lsp.instToJsonResolvableCompletionItem : ToJson ResolvableCompletionItem

def Lean.Lsp.instToJsonResolvableCompletionItem.toJson : ResolvableCompletionItem → Json

instance Lean.Lsp.instInhabitedResolvableCompletionItem : Inhabited ResolvableCompletionItem

def Lean.Lsp.instInhabitedResolvableCompletionItem.default : ResolvableCompletionItem

instance Lean.Lsp.instBEqResolvableCompletionItem : BEq ResolvableCompletionItem

def Lean.Lsp.instBEqResolvableCompletionItem.beq : ResolvableCompletionItem → ResolvableCompletionItem → Bool

instance Lean.Lsp.instHashableResolvableCompletionItem : Hashable ResolvableCompletionItem

def Lean.Lsp.instHashableResolvableCompletionItem.hash : ResolvableCompletionItem → UInt64

structure Lean.Lsp.ResolvableCompletionList : Type

• isIncomplete : Bool
• items : Array ResolvableCompletionItem

def Lean.Lsp.instFromJsonResolvableCompletionList.fromJson : Json → Except String ResolvableCompletionList

instance Lean.Lsp.instFromJsonResolvableCompletionList : FromJson ResolvableCompletionList

instance Lean.Lsp.instToJsonResolvableCompletionList : ToJson ResolvableCompletionList

def Lean.Lsp.instToJsonResolvableCompletionList.toJson : ResolvableCompletionList → Json

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

• textDocument : TextDocumentIdentifier
• position : Position

def Lean.Lsp.instFromJsonCompletionParams.fromJson : Json → Except String CompletionParams

instance Lean.Lsp.instFromJsonCompletionParams : FromJson CompletionParams

def Lean.Lsp.instToJsonCompletionParams.toJson : CompletionParams → Json

instance Lean.Lsp.instToJsonCompletionParams : ToJson CompletionParams

structure Lean.Lsp.Hover : Type

• contents : MarkupContent
• range? : Option Range

instance Lean.Lsp.instToJsonHover : ToJson Hover

def Lean.Lsp.instToJsonHover.toJson : Hover → Json

instance Lean.Lsp.instFromJsonHover : FromJson Hover

def Lean.Lsp.instFromJsonHover.fromJson : Json → Except String Hover

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

• textDocument : TextDocumentIdentifier
• position : Position

def Lean.Lsp.instFromJsonHoverParams.fromJson : Json → Except String HoverParams

instance Lean.Lsp.instFromJsonHoverParams : FromJson HoverParams

def Lean.Lsp.instToJsonHoverParams.toJson : HoverParams → Json

instance Lean.Lsp.instToJsonHoverParams : ToJson HoverParams

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

• textDocument : TextDocumentIdentifier
• position : Position

instance Lean.Lsp.instFromJsonDeclarationParams : FromJson DeclarationParams

def Lean.Lsp.instFromJsonDeclarationParams.fromJson : Json → Except String DeclarationParams

instance Lean.Lsp.instToJsonDeclarationParams : ToJson DeclarationParams

def Lean.Lsp.instToJsonDeclarationParams.toJson : DeclarationParams → Json

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

• textDocument : TextDocumentIdentifier
• position : Position

def Lean.Lsp.instFromJsonDefinitionParams.fromJson : Json → Except String DefinitionParams

instance Lean.Lsp.instFromJsonDefinitionParams : FromJson DefinitionParams

def Lean.Lsp.instToJsonDefinitionParams.toJson : DefinitionParams → Json

instance Lean.Lsp.instToJsonDefinitionParams : ToJson DefinitionParams

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

• textDocument : TextDocumentIdentifier
• position : Position

instance Lean.Lsp.instFromJsonTypeDefinitionParams : FromJson TypeDefinitionParams

def Lean.Lsp.instFromJsonTypeDefinitionParams.fromJson : Json → Except String TypeDefinitionParams

def Lean.Lsp.instToJsonTypeDefinitionParams.toJson : TypeDefinitionParams → Json

instance Lean.Lsp.instToJsonTypeDefinitionParams : ToJson TypeDefinitionParams

structure Lean.Lsp.ReferenceContext : Type

• includeDeclaration : Bool

def Lean.Lsp.instFromJsonReferenceContext.fromJson : Json → Except String ReferenceContext

instance Lean.Lsp.instFromJsonReferenceContext : FromJson ReferenceContext

def Lean.Lsp.instToJsonReferenceContext.toJson : ReferenceContext → Json

instance Lean.Lsp.instToJsonReferenceContext : ToJson ReferenceContext

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

• textDocument : TextDocumentIdentifier
• position : Position
• context : ReferenceContext

instance Lean.Lsp.instFromJsonReferenceParams : FromJson ReferenceParams

def Lean.Lsp.instFromJsonReferenceParams.fromJson : Json → Except String ReferenceParams

instance Lean.Lsp.instToJsonReferenceParams : ToJson ReferenceParams

def Lean.Lsp.instToJsonReferenceParams.toJson : ReferenceParams → Json

structure Lean.Lsp.WorkspaceSymbolParams : Type

• query : String

instance Lean.Lsp.instFromJsonWorkspaceSymbolParams : FromJson WorkspaceSymbolParams

def Lean.Lsp.instFromJsonWorkspaceSymbolParams.fromJson : Json → Except String WorkspaceSymbolParams

instance Lean.Lsp.instToJsonWorkspaceSymbolParams : ToJson WorkspaceSymbolParams

def Lean.Lsp.instToJsonWorkspaceSymbolParams.toJson : WorkspaceSymbolParams → Json

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

• textDocument : TextDocumentIdentifier
• position : Position

instance Lean.Lsp.instFromJsonDocumentHighlightParams : FromJson DocumentHighlightParams

def Lean.Lsp.instFromJsonDocumentHighlightParams.fromJson : Json → Except String DocumentHighlightParams

instance Lean.Lsp.instToJsonDocumentHighlightParams : ToJson DocumentHighlightParams

def Lean.Lsp.instToJsonDocumentHighlightParams.toJson : DocumentHighlightParams → Json

inductive Lean.Lsp.DocumentHighlightKind : Type

• text : DocumentHighlightKind
• read : DocumentHighlightKind
• write : DocumentHighlightKind

instance Lean.Lsp.instToJsonDocumentHighlightKind : ToJson DocumentHighlightKind

structure Lean.Lsp.DocumentHighlight : Type

• range : Range
• kind? : Option DocumentHighlightKind

instance Lean.Lsp.instToJsonDocumentHighlight : ToJson DocumentHighlight

def Lean.Lsp.instToJsonDocumentHighlight.toJson : DocumentHighlight → Json

@[reducible, inline]

abbrev Lean.Lsp.DocumentHighlightResult : Type

structure Lean.Lsp.DocumentSymbolParams : Type

• textDocument : TextDocumentIdentifier

instance Lean.Lsp.instFromJsonDocumentSymbolParams : FromJson DocumentSymbolParams

def Lean.Lsp.instFromJsonDocumentSymbolParams.fromJson : Json → Except String DocumentSymbolParams

instance Lean.Lsp.instToJsonDocumentSymbolParams : ToJson DocumentSymbolParams

def Lean.Lsp.instToJsonDocumentSymbolParams.toJson : DocumentSymbolParams → Json

inductive Lean.Lsp.SymbolKind : Type

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

def Lean.Lsp.instBEqSymbolKind.beq : SymbolKind → SymbolKind → Bool

instance Lean.Lsp.instBEqSymbolKind : BEq SymbolKind

def Lean.Lsp.instHashableSymbolKind.hash : SymbolKind → UInt64

instance Lean.Lsp.instHashableSymbolKind : Hashable SymbolKind

def Lean.Lsp.instInhabitedSymbolKind.default : SymbolKind

instance Lean.Lsp.instInhabitedSymbolKind : Inhabited SymbolKind

instance Lean.Lsp.instFromJsonSymbolKind : FromJson SymbolKind

instance Lean.Lsp.instToJsonSymbolKind : ToJson SymbolKind

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

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

def Lean.Lsp.instFromJsonDocumentSymbolAux.fromJson {Self✝ : Type} [FromJson Self✝] : Json → Except String (DocumentSymbolAux Self✝)

instance Lean.Lsp.instFromJsonDocumentSymbolAux {Self✝ : Type} [FromJson Self✝] : FromJson (DocumentSymbolAux Self✝)

def Lean.Lsp.instToJsonDocumentSymbolAux.toJson {Self✝ : Type} [ToJson Self✝] : DocumentSymbolAux Self✝ → Json

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

inductive Lean.Lsp.DocumentSymbol : Type

• mk (sym : DocumentSymbolAux DocumentSymbol) : DocumentSymbol

instance Lean.Lsp.instToJsonDocumentSymbol : ToJson DocumentSymbol

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

structure Lean.Lsp.DocumentSymbolResult : Type

• syms : Array DocumentSymbol

instance Lean.Lsp.instToJsonDocumentSymbolResult : ToJson DocumentSymbolResult

inductive Lean.Lsp.SymbolTag : Type

• deprecated : SymbolTag

def Lean.Lsp.instBEqSymbolTag.beq : SymbolTag → SymbolTag → Bool

instance Lean.Lsp.instBEqSymbolTag : BEq SymbolTag

def Lean.Lsp.instHashableSymbolTag.hash : SymbolTag → UInt64

instance Lean.Lsp.instHashableSymbolTag : Hashable SymbolTag

instance Lean.Lsp.instInhabitedSymbolTag : Inhabited SymbolTag

def Lean.Lsp.instInhabitedSymbolTag.default : SymbolTag

instance Lean.Lsp.instFromJsonSymbolTag : FromJson SymbolTag

instance Lean.Lsp.instToJsonSymbolTag : ToJson SymbolTag

structure Lean.Lsp.SymbolInformation : Type

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

def Lean.Lsp.instFromJsonSymbolInformation.fromJson : Json → Except String SymbolInformation

instance Lean.Lsp.instFromJsonSymbolInformation : FromJson SymbolInformation

instance Lean.Lsp.instToJsonSymbolInformation : ToJson SymbolInformation

def Lean.Lsp.instToJsonSymbolInformation.toJson : SymbolInformation → Json

structure Lean.Lsp.CallHierarchyPrepareParamsextends Lean.Lsp.TextDocumentPositionParams : Type

• textDocument : TextDocumentIdentifier
• position : Position

instance Lean.Lsp.instFromJsonCallHierarchyPrepareParams : FromJson CallHierarchyPrepareParams

def Lean.Lsp.instFromJsonCallHierarchyPrepareParams.fromJson : Json → Except String CallHierarchyPrepareParams

def Lean.Lsp.instToJsonCallHierarchyPrepareParams.toJson : CallHierarchyPrepareParams → Json

instance Lean.Lsp.instToJsonCallHierarchyPrepareParams : ToJson CallHierarchyPrepareParams

structure Lean.Lsp.CallHierarchyItem : Type

• name : String
• kind : SymbolKind
• tags? : Option (Array SymbolTag)
• detail? : Option String
• uri : DocumentUri
• range : Range
• selectionRange : Range
• data? : Option Json

instance Lean.Lsp.instFromJsonCallHierarchyItem : FromJson CallHierarchyItem

def Lean.Lsp.instFromJsonCallHierarchyItem.fromJson : Json → Except String CallHierarchyItem

instance Lean.Lsp.instToJsonCallHierarchyItem : ToJson CallHierarchyItem

def Lean.Lsp.instToJsonCallHierarchyItem.toJson : CallHierarchyItem → Json

def Lean.Lsp.instBEqCallHierarchyItem.beq : CallHierarchyItem → CallHierarchyItem → Bool

instance Lean.Lsp.instBEqCallHierarchyItem : BEq CallHierarchyItem

instance Lean.Lsp.instHashableCallHierarchyItem : Hashable CallHierarchyItem

def Lean.Lsp.instHashableCallHierarchyItem.hash : CallHierarchyItem → UInt64

instance Lean.Lsp.instInhabitedCallHierarchyItem : Inhabited CallHierarchyItem

def Lean.Lsp.instInhabitedCallHierarchyItem.default : CallHierarchyItem

structure Lean.Lsp.CallHierarchyIncomingCallsParams : Type

• item : CallHierarchyItem

def Lean.Lsp.instFromJsonCallHierarchyIncomingCallsParams.fromJson : Json → Except String CallHierarchyIncomingCallsParams

instance Lean.Lsp.instFromJsonCallHierarchyIncomingCallsParams : FromJson CallHierarchyIncomingCallsParams

def Lean.Lsp.instToJsonCallHierarchyIncomingCallsParams.toJson : CallHierarchyIncomingCallsParams → Json

instance Lean.Lsp.instToJsonCallHierarchyIncomingCallsParams : ToJson CallHierarchyIncomingCallsParams

structure Lean.Lsp.CallHierarchyIncomingCall : Type

• from : CallHierarchyItem
• fromRanges : Array Range

instance Lean.Lsp.instFromJsonCallHierarchyIncomingCall : FromJson CallHierarchyIncomingCall

def Lean.Lsp.instFromJsonCallHierarchyIncomingCall.fromJson : Json → Except String CallHierarchyIncomingCall

def Lean.Lsp.instToJsonCallHierarchyIncomingCall.toJson : CallHierarchyIncomingCall → Json

instance Lean.Lsp.instToJsonCallHierarchyIncomingCall : ToJson CallHierarchyIncomingCall

def Lean.Lsp.instInhabitedCallHierarchyIncomingCall.default : CallHierarchyIncomingCall

instance Lean.Lsp.instInhabitedCallHierarchyIncomingCall : Inhabited CallHierarchyIncomingCall

structure Lean.Lsp.CallHierarchyOutgoingCallsParams : Type

• item : CallHierarchyItem

def Lean.Lsp.instFromJsonCallHierarchyOutgoingCallsParams.fromJson : Json → Except String CallHierarchyOutgoingCallsParams

instance Lean.Lsp.instFromJsonCallHierarchyOutgoingCallsParams : FromJson CallHierarchyOutgoingCallsParams

instance Lean.Lsp.instToJsonCallHierarchyOutgoingCallsParams : ToJson CallHierarchyOutgoingCallsParams

def Lean.Lsp.instToJsonCallHierarchyOutgoingCallsParams.toJson : CallHierarchyOutgoingCallsParams → Json

structure Lean.Lsp.CallHierarchyOutgoingCall : Type

• to : CallHierarchyItem
• fromRanges : Array Range

def Lean.Lsp.instFromJsonCallHierarchyOutgoingCall.fromJson : Json → Except String CallHierarchyOutgoingCall

instance Lean.Lsp.instFromJsonCallHierarchyOutgoingCall : FromJson CallHierarchyOutgoingCall

instance Lean.Lsp.instToJsonCallHierarchyOutgoingCall : ToJson CallHierarchyOutgoingCall

def Lean.Lsp.instToJsonCallHierarchyOutgoingCall.toJson : CallHierarchyOutgoingCall → Json

instance Lean.Lsp.instInhabitedCallHierarchyOutgoingCall : Inhabited CallHierarchyOutgoingCall

def Lean.Lsp.instInhabitedCallHierarchyOutgoingCall.default : CallHierarchyOutgoingCall

inductive Lean.Lsp.SemanticTokenType : Type

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

instance Lean.Lsp.instToJsonSemanticTokenType : ToJson SemanticTokenType

def Lean.Lsp.instToJsonSemanticTokenType.toJson : SemanticTokenType → Json

instance Lean.Lsp.instFromJsonSemanticTokenType : FromJson SemanticTokenType

def Lean.Lsp.instFromJsonSemanticTokenType.fromJson : Json → Except String SemanticTokenType

def Lean.Lsp.instBEqSemanticTokenType.beq : SemanticTokenType → SemanticTokenType → Bool

instance Lean.Lsp.instBEqSemanticTokenType : BEq SemanticTokenType

instance Lean.Lsp.instHashableSemanticTokenType : Hashable SemanticTokenType

def Lean.Lsp.instHashableSemanticTokenType.hash : SemanticTokenType → UInt64

def Lean.Lsp.SemanticTokenType.names : Array String

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

inductive Lean.Lsp.SemanticTokenModifier : Type

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.

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

def Lean.Lsp.instToJsonSemanticTokenModifier.toJson : SemanticTokenModifier → Json

instance Lean.Lsp.instToJsonSemanticTokenModifier : ToJson SemanticTokenModifier

instance Lean.Lsp.instFromJsonSemanticTokenModifier : FromJson SemanticTokenModifier

def Lean.Lsp.instFromJsonSemanticTokenModifier.fromJson : Json → Except String SemanticTokenModifier

def Lean.Lsp.SemanticTokenModifier.names : Array String

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

structure Lean.Lsp.SemanticTokensLegend : Type

• tokenTypes : Array String
• tokenModifiers : Array String

def Lean.Lsp.instFromJsonSemanticTokensLegend.fromJson : Json → Except String SemanticTokensLegend

instance Lean.Lsp.instFromJsonSemanticTokensLegend : FromJson SemanticTokensLegend

instance Lean.Lsp.instToJsonSemanticTokensLegend : ToJson SemanticTokensLegend

def Lean.Lsp.instToJsonSemanticTokensLegend.toJson : SemanticTokensLegend → Json

structure Lean.Lsp.SemanticTokensOptions : Type

• legend : SemanticTokensLegend
• range : Bool
• full : Bool

instance Lean.Lsp.instFromJsonSemanticTokensOptions : FromJson SemanticTokensOptions

def Lean.Lsp.instFromJsonSemanticTokensOptions.fromJson : Json → Except String SemanticTokensOptions

instance Lean.Lsp.instToJsonSemanticTokensOptions : ToJson SemanticTokensOptions

def Lean.Lsp.instToJsonSemanticTokensOptions.toJson : SemanticTokensOptions → Json

structure Lean.Lsp.SemanticTokensParams : Type

• textDocument : TextDocumentIdentifier

def Lean.Lsp.instFromJsonSemanticTokensParams.fromJson : Json → Except String SemanticTokensParams

instance Lean.Lsp.instFromJsonSemanticTokensParams : FromJson SemanticTokensParams

def Lean.Lsp.instToJsonSemanticTokensParams.toJson : SemanticTokensParams → Json

instance Lean.Lsp.instToJsonSemanticTokensParams : ToJson SemanticTokensParams

structure Lean.Lsp.SemanticTokensRangeParams : Type

• textDocument : TextDocumentIdentifier
• range : Range

instance Lean.Lsp.instFromJsonSemanticTokensRangeParams : FromJson SemanticTokensRangeParams

def Lean.Lsp.instFromJsonSemanticTokensRangeParams.fromJson : Json → Except String SemanticTokensRangeParams

def Lean.Lsp.instToJsonSemanticTokensRangeParams.toJson : SemanticTokensRangeParams → Json

instance Lean.Lsp.instToJsonSemanticTokensRangeParams : ToJson SemanticTokensRangeParams

structure Lean.Lsp.SemanticTokens : Type

• resultId? : Option String
• data : Array Nat

instance Lean.Lsp.instFromJsonSemanticTokens : FromJson SemanticTokens

def Lean.Lsp.instFromJsonSemanticTokens.fromJson : Json → Except String SemanticTokens

def Lean.Lsp.instToJsonSemanticTokens.toJson : SemanticTokens → Json

instance Lean.Lsp.instToJsonSemanticTokens : ToJson SemanticTokens

structure Lean.Lsp.FoldingRangeParams : Type

• textDocument : TextDocumentIdentifier

def Lean.Lsp.instFromJsonFoldingRangeParams.fromJson : Json → Except String FoldingRangeParams

instance Lean.Lsp.instFromJsonFoldingRangeParams : FromJson FoldingRangeParams

def Lean.Lsp.instToJsonFoldingRangeParams.toJson : FoldingRangeParams → Json

instance Lean.Lsp.instToJsonFoldingRangeParams : ToJson FoldingRangeParams

inductive Lean.Lsp.FoldingRangeKind : Type

• comment : FoldingRangeKind
• imports : FoldingRangeKind
• region : FoldingRangeKind

instance Lean.Lsp.instToJsonFoldingRangeKind : ToJson FoldingRangeKind

structure Lean.Lsp.FoldingRange : Type

• startLine : Nat
• endLine : Nat
• kind? : Option FoldingRangeKind

instance Lean.Lsp.instToJsonFoldingRange : ToJson FoldingRange

def Lean.Lsp.instToJsonFoldingRange.toJson : FoldingRange → Json

structure Lean.Lsp.RenameOptions : Type

• prepareProvider : Bool

def Lean.Lsp.instFromJsonRenameOptions.fromJson : Json → Except String RenameOptions

instance Lean.Lsp.instFromJsonRenameOptions : FromJson RenameOptions

instance Lean.Lsp.instToJsonRenameOptions : ToJson RenameOptions

def Lean.Lsp.instToJsonRenameOptions.toJson : RenameOptions → Json

structure Lean.Lsp.RenameParamsextends Lean.Lsp.TextDocumentPositionParams : Type

• textDocument : TextDocumentIdentifier
• position : Position
• newName : String

instance Lean.Lsp.instFromJsonRenameParams : FromJson RenameParams

def Lean.Lsp.instFromJsonRenameParams.fromJson : Json → Except String RenameParams

instance Lean.Lsp.instToJsonRenameParams : ToJson RenameParams

def Lean.Lsp.instToJsonRenameParams.toJson : RenameParams → Json

structure Lean.Lsp.PrepareRenameParamsextends Lean.Lsp.TextDocumentPositionParams : Type

• textDocument : TextDocumentIdentifier
• position : Position

def Lean.Lsp.instFromJsonPrepareRenameParams.fromJson : Json → Except String PrepareRenameParams

instance Lean.Lsp.instFromJsonPrepareRenameParams : FromJson PrepareRenameParams

def Lean.Lsp.instToJsonPrepareRenameParams.toJson : PrepareRenameParams → Json

instance Lean.Lsp.instToJsonPrepareRenameParams : ToJson PrepareRenameParams

structure Lean.Lsp.InlayHintParamsextends Lean.Lsp.WorkDoneProgressParams : Type

• workDoneToken? : Option ProgressToken
• textDocument : TextDocumentIdentifier
• range : Range

instance Lean.Lsp.instFromJsonInlayHintParams : FromJson InlayHintParams

def Lean.Lsp.instFromJsonInlayHintParams.fromJson : Json → Except String InlayHintParams

def Lean.Lsp.instToJsonInlayHintParams.toJson : InlayHintParams → Json

instance Lean.Lsp.instToJsonInlayHintParams : ToJson InlayHintParams

inductive Lean.Lsp.InlayHintTooltip : Type

• plaintext (text : String) : InlayHintTooltip
• markdown (markup : MarkupContent) : InlayHintTooltip

instance Lean.Lsp.instFromJsonInlayHintTooltip : FromJson InlayHintTooltip

instance Lean.Lsp.instToJsonInlayHintTooltip : ToJson InlayHintTooltip

structure Lean.Lsp.InlayHintLabelPart : Type

• value : String
• tooltip? : Option InlayHintTooltip
• location? : Option Location
• command? : Option Command

def Lean.Lsp.instFromJsonInlayHintLabelPart.fromJson : Json → Except String InlayHintLabelPart

instance Lean.Lsp.instFromJsonInlayHintLabelPart : FromJson InlayHintLabelPart

instance Lean.Lsp.instToJsonInlayHintLabelPart : ToJson InlayHintLabelPart

def Lean.Lsp.instToJsonInlayHintLabelPart.toJson : InlayHintLabelPart → Json

inductive Lean.Lsp.InlayHintLabel : Type

• name (n : String) : InlayHintLabel
• parts (p : Array InlayHintLabelPart) : InlayHintLabel

instance Lean.Lsp.instFromJsonInlayHintLabel : FromJson InlayHintLabel

instance Lean.Lsp.instToJsonInlayHintLabel : ToJson InlayHintLabel

inductive Lean.Lsp.InlayHintKind : Type

• type : InlayHintKind
• parameter : InlayHintKind

instance Lean.Lsp.instFromJsonInlayHintKind : FromJson InlayHintKind

instance Lean.Lsp.instToJsonInlayHintKind : ToJson InlayHintKind

structure Lean.Lsp.InlayHint : Type

• position : Position
• label : InlayHintLabel
• kind? : Option InlayHintKind
• textEdits? : Option (Array TextEdit)
• tooltip? : Option InlayHintTooltip
• paddingLeft? : Option Bool
• paddingRight? : Option Bool
• data? : Option Json

def Lean.Lsp.instFromJsonInlayHint.fromJson : Json → Except String InlayHint

instance Lean.Lsp.instFromJsonInlayHint : FromJson InlayHint

instance Lean.Lsp.instToJsonInlayHint : ToJson InlayHint

def Lean.Lsp.instToJsonInlayHint.toJson : InlayHint → Json

structure Lean.Lsp.InlayHintClientCapabilities : Type

• dynamicRegistration? : Option Bool
• resolveSupport? : Option ResolveSupport

instance Lean.Lsp.instFromJsonInlayHintClientCapabilities : FromJson InlayHintClientCapabilities

def Lean.Lsp.instFromJsonInlayHintClientCapabilities.fromJson : Json → Except String InlayHintClientCapabilities

instance Lean.Lsp.instToJsonInlayHintClientCapabilities : ToJson InlayHintClientCapabilities

def Lean.Lsp.instToJsonInlayHintClientCapabilities.toJson : InlayHintClientCapabilities → Json

structure Lean.Lsp.InlayHintOptionsextends Lean.Lsp.WorkDoneProgressOptions : Type

• workDoneProgress : Bool
• resolveProvider? : Option Bool

instance Lean.Lsp.instFromJsonInlayHintOptions : FromJson InlayHintOptions

def Lean.Lsp.instFromJsonInlayHintOptions.fromJson : Json → Except String InlayHintOptions

instance Lean.Lsp.instToJsonInlayHintOptions : ToJson InlayHintOptions

def Lean.Lsp.instToJsonInlayHintOptions.toJson : InlayHintOptions → Json

inductive Lean.Lsp.ParameterInformationLabel : Type

• name (name : String) : ParameterInformationLabel
• range (startUtf16Offset endUtf16Offset : Nat) : ParameterInformationLabel

instance Lean.Lsp.instFromJsonParameterInformationLabel : FromJson ParameterInformationLabel

instance Lean.Lsp.instToJsonParameterInformationLabel : ToJson ParameterInformationLabel

structure Lean.Lsp.ParameterInformation : Type

• label : ParameterInformationLabel
• documentation? : Option MarkupContent

instance Lean.Lsp.instFromJsonParameterInformation : FromJson ParameterInformation

def Lean.Lsp.instFromJsonParameterInformation.fromJson : Json → Except String ParameterInformation

instance Lean.Lsp.instToJsonParameterInformation : ToJson ParameterInformation

def Lean.Lsp.instToJsonParameterInformation.toJson : ParameterInformation → Json

structure Lean.Lsp.SignatureInformation : Type

• label : String
• documentation? : Option MarkupContent
• parameters? : Option (Array ParameterInformation)
• activeParameter? : Option Nat

def Lean.Lsp.instFromJsonSignatureInformation.fromJson : Json → Except String SignatureInformation

instance Lean.Lsp.instFromJsonSignatureInformation : FromJson SignatureInformation

def Lean.Lsp.instToJsonSignatureInformation.toJson : SignatureInformation → Json

instance Lean.Lsp.instToJsonSignatureInformation : ToJson SignatureInformation

structure Lean.Lsp.SignatureHelp : Type

• signatures : Array SignatureInformation
• activeSignature? : Option Nat
• activeParameter? : Option Nat

instance Lean.Lsp.instFromJsonSignatureHelp : FromJson SignatureHelp

def Lean.Lsp.instFromJsonSignatureHelp.fromJson : Json → Except String SignatureHelp

def Lean.Lsp.instToJsonSignatureHelp.toJson : SignatureHelp → Json

instance Lean.Lsp.instToJsonSignatureHelp : ToJson SignatureHelp

inductive Lean.Lsp.SignatureHelpTriggerKind : Type

• invoked : SignatureHelpTriggerKind
• triggerCharacter : SignatureHelpTriggerKind
• contentChange : SignatureHelpTriggerKind

instance Lean.Lsp.instFromJsonSignatureHelpTriggerKind : FromJson SignatureHelpTriggerKind

instance Lean.Lsp.instToJsonSignatureHelpTriggerKind : ToJson SignatureHelpTriggerKind

structure Lean.Lsp.SignatureHelpContext : Type

• triggerKind : SignatureHelpTriggerKind
• triggerCharacter? : Option String
• isRetrigger : Bool
• activeSignatureHelp? : Option SignatureHelp

instance Lean.Lsp.instFromJsonSignatureHelpContext : FromJson SignatureHelpContext

def Lean.Lsp.instFromJsonSignatureHelpContext.fromJson : Json → Except String SignatureHelpContext

def Lean.Lsp.instToJsonSignatureHelpContext.toJson : SignatureHelpContext → Json

instance Lean.Lsp.instToJsonSignatureHelpContext : ToJson SignatureHelpContext

structure Lean.Lsp.SignatureHelpParamsextends Lean.Lsp.TextDocumentPositionParams, Lean.Lsp.WorkDoneProgressParams : Type

• textDocument : TextDocumentIdentifier
• position : Position
• workDoneToken? : Option ProgressToken
• context? : Option SignatureHelpContext

instance Lean.Lsp.instFromJsonSignatureHelpParams : FromJson SignatureHelpParams

def Lean.Lsp.instFromJsonSignatureHelpParams.fromJson : Json → Except String SignatureHelpParams

def Lean.Lsp.instToJsonSignatureHelpParams.toJson : SignatureHelpParams → Json

instance Lean.Lsp.instToJsonSignatureHelpParams : ToJson SignatureHelpParams

structure Lean.Lsp.SignatureHelpOptionsextends Lean.Lsp.WorkDoneProgressOptions : Type

• workDoneProgress : Bool
• triggerCharacters? : Option (Array String)
• retriggerCharacters? : Option (Array String)

def Lean.Lsp.instFromJsonSignatureHelpOptions.fromJson : Json → Except String SignatureHelpOptions

instance Lean.Lsp.instFromJsonSignatureHelpOptions : FromJson SignatureHelpOptions

def Lean.Lsp.instToJsonSignatureHelpOptions.toJson : SignatureHelpOptions → Json

instance Lean.Lsp.instToJsonSignatureHelpOptions : ToJson SignatureHelpOptions

structure Lean.Lsp.DocumentColorParamsextends Lean.Lsp.WorkDoneProgressParams, Lean.Lsp.PartialResultParams : Type

• workDoneToken? : Option ProgressToken
• partialResultToken? : Option ProgressToken
• textDocument : TextDocumentIdentifier

instance Lean.Lsp.instFromJsonDocumentColorParams : FromJson DocumentColorParams

def Lean.Lsp.instFromJsonDocumentColorParams.fromJson : Json → Except String DocumentColorParams

instance Lean.Lsp.instToJsonDocumentColorParams : ToJson DocumentColorParams

def Lean.Lsp.instToJsonDocumentColorParams.toJson : DocumentColorParams → Json

structure Lean.Lsp.Color : Type

• red : Float
• green : Float
• blue : Float
• alpha : Float

instance Lean.Lsp.instFromJsonColor : FromJson Color

def Lean.Lsp.instFromJsonColor.fromJson : Json → Except String Color

def Lean.Lsp.instToJsonColor.toJson : Color → Json

instance Lean.Lsp.instToJsonColor : ToJson Color

structure Lean.Lsp.ColorInformation : Type

• range : Range
• color : Color

def Lean.Lsp.instFromJsonColorInformation.fromJson : Json → Except String ColorInformation

instance Lean.Lsp.instFromJsonColorInformation : FromJson ColorInformation

instance Lean.Lsp.instToJsonColorInformation : ToJson ColorInformation

def Lean.Lsp.instToJsonColorInformation.toJson : ColorInformation → Json

structure Lean.Lsp.DocumentColorOptionsextends Lean.Lsp.WorkDoneProgressOptions : Type

• workDoneProgress : Bool

instance Lean.Lsp.instFromJsonDocumentColorOptions : FromJson DocumentColorOptions

def Lean.Lsp.instFromJsonDocumentColorOptions.fromJson : Json → Except String DocumentColorOptions

def Lean.Lsp.instToJsonDocumentColorOptions.toJson : DocumentColorOptions → Json

instance Lean.Lsp.instToJsonDocumentColorOptions : ToJson DocumentColorOptions