structure Lean.Lsp.CompletionOptions : Type

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonCompletionOptions : FromJson CompletionOptions

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instInhabitedCompletionItemKind : Inhabited CompletionItemKind

def Lean.Lsp.instInhabitedCompletionItemKind.default : CompletionItemKind

@[implicit_reducible]

instance Lean.Lsp.instDecidableEqCompletionItemKind : DecidableEq CompletionItemKind

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

@[implicit_reducible]

instance Lean.Lsp.instReprCompletionItemKind : Repr CompletionItemKind

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

@[implicit_reducible]

instance Lean.Lsp.instHashableCompletionItemKind : Hashable CompletionItemKind

@[implicit_reducible]

instance Lean.Lsp.instToJsonCompletionItemKind : ToJson CompletionItemKind

@[implicit_reducible]

instance Lean.Lsp.instFromJsonCompletionItemKind : FromJson CompletionItemKind

structure Lean.Lsp.InsertReplaceEdit : Type

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonInsertReplaceEdit : FromJson InsertReplaceEdit

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

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonInsertReplaceEdit : ToJson InsertReplaceEdit

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

@[implicit_reducible]

instance Lean.Lsp.instBEqInsertReplaceEdit : BEq InsertReplaceEdit

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

@[implicit_reducible]

instance Lean.Lsp.instHashableInsertReplaceEdit : Hashable InsertReplaceEdit

inductive Lean.Lsp.CompletionItemTag : Type

• deprecated : CompletionItemTag

@[implicit_reducible]

instance Lean.Lsp.instInhabitedCompletionItemTag : Inhabited CompletionItemTag

def Lean.Lsp.instInhabitedCompletionItemTag.default : CompletionItemTag

@[implicit_reducible]

instance Lean.Lsp.instDecidableEqCompletionItemTag : DecidableEq CompletionItemTag

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

@[implicit_reducible]

instance Lean.Lsp.instReprCompletionItemTag : Repr CompletionItemTag

@[implicit_reducible]

instance Lean.Lsp.instHashableCompletionItemTag : Hashable CompletionItemTag

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonCompletionItemTag : ToJson CompletionItemTag

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonCompletionItem : FromJson CompletionItem

@[implicit_reducible]

instance Lean.Lsp.instToJsonCompletionItem : ToJson CompletionItem

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

def Lean.Lsp.instInhabitedCompletionItem.default : CompletionItem

@[implicit_reducible]

instance Lean.Lsp.instInhabitedCompletionItem : Inhabited CompletionItem

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

@[implicit_reducible]

instance Lean.Lsp.instBEqCompletionItem : BEq CompletionItem

@[implicit_reducible]

instance Lean.Lsp.instHashableCompletionItem : Hashable CompletionItem

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

structure Lean.Lsp.CompletionList : Type

• isIncomplete : Bool
• items : Array CompletionItem

@[implicit_reducible]

instance Lean.Lsp.instFromJsonCompletionList : FromJson CompletionList

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

@[implicit_reducible]

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

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

@[implicit_reducible]

instance Lean.Lsp.instBEqCompletionIdentifier : BEq CompletionIdentifier

@[implicit_reducible]

instance Lean.Lsp.instHashableCompletionIdentifier : Hashable CompletionIdentifier

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonCompletionIdentifier : ToJson CompletionIdentifier

@[implicit_reducible]

instance Lean.Lsp.instFromJsonCompletionIdentifier : FromJson CompletionIdentifier

structure Lean.Lsp.ResolvableCompletionItemData : Type

• uri : DocumentUri
• pos : Position
• cPos? : Option Nat

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

• id? : Option CompletionIdentifier

@[implicit_reducible]

instance Lean.Lsp.instBEqResolvableCompletionItemData : BEq ResolvableCompletionItemData

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

@[implicit_reducible]

instance Lean.Lsp.instHashableResolvableCompletionItemData : Hashable ResolvableCompletionItemData

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonResolvableCompletionItemData : ToJson ResolvableCompletionItemData

@[implicit_reducible]

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)

@[implicit_reducible]

instance Lean.Lsp.instFromJsonResolvableCompletionItem : FromJson ResolvableCompletionItem

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonResolvableCompletionItem : ToJson ResolvableCompletionItem

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

@[implicit_reducible]

instance Lean.Lsp.instInhabitedResolvableCompletionItem : Inhabited ResolvableCompletionItem

def Lean.Lsp.instInhabitedResolvableCompletionItem.default : ResolvableCompletionItem

@[implicit_reducible]

instance Lean.Lsp.instBEqResolvableCompletionItem : BEq ResolvableCompletionItem

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

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

@[implicit_reducible]

instance Lean.Lsp.instHashableResolvableCompletionItem : Hashable ResolvableCompletionItem

structure Lean.Lsp.ResolvableCompletionList : Type

• isIncomplete : Bool
• items : Array ResolvableCompletionItem

@[implicit_reducible]

instance Lean.Lsp.instFromJsonResolvableCompletionList : FromJson ResolvableCompletionList

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

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonResolvableCompletionList : ToJson ResolvableCompletionList

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

• textDocument : TextDocumentIdentifier
• position : Position

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonCompletionParams : FromJson CompletionParams

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonCompletionParams : ToJson CompletionParams

structure Lean.Lsp.Hover : Type

• contents : MarkupContent
• range? : Option Range

@[implicit_reducible]

instance Lean.Lsp.instToJsonHover : ToJson Hover

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

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonHover : FromJson Hover

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

• textDocument : TextDocumentIdentifier
• position : Position

@[implicit_reducible]

instance Lean.Lsp.instFromJsonHoverParams : FromJson HoverParams

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

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonHoverParams : ToJson HoverParams

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

• textDocument : TextDocumentIdentifier
• position : Position

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDeclarationParams : FromJson DeclarationParams

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDefinitionParams : FromJson DefinitionParams

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonDefinitionParams : ToJson DefinitionParams

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

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

• textDocument : TextDocumentIdentifier
• position : Position

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonTypeDefinitionParams : FromJson TypeDefinitionParams

@[implicit_reducible]

instance Lean.Lsp.instToJsonTypeDefinitionParams : ToJson TypeDefinitionParams

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

structure Lean.Lsp.ReferenceContext : Type

• includeDeclaration : Bool

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonReferenceContext : FromJson ReferenceContext

@[implicit_reducible]

instance Lean.Lsp.instToJsonReferenceContext : ToJson ReferenceContext

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

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

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonReferenceParams : FromJson ReferenceParams

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonReferenceParams : ToJson ReferenceParams

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

structure Lean.Lsp.WorkspaceSymbolParams : Type

• query : String

@[implicit_reducible]

instance Lean.Lsp.instFromJsonWorkspaceSymbolParams : FromJson WorkspaceSymbolParams

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDocumentHighlightParams : FromJson DocumentHighlightParams

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonDocumentHighlightParams : ToJson DocumentHighlightParams

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

inductive Lean.Lsp.DocumentHighlightKind : Type

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonDocumentHighlightKind : ToJson DocumentHighlightKind

structure Lean.Lsp.DocumentHighlight : Type

• range : Range
• kind? : Option DocumentHighlightKind

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonDocumentHighlight : ToJson DocumentHighlight

@[reducible, inline]

abbrev Lean.Lsp.DocumentHighlightResult : Type

structure Lean.Lsp.DocumentSymbolParams : Type

• textDocument : TextDocumentIdentifier

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDocumentSymbolParams : FromJson DocumentSymbolParams

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

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonDocumentSymbolParams : ToJson DocumentSymbolParams

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

@[implicit_reducible]

instance Lean.Lsp.instBEqSymbolKind : BEq SymbolKind

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

@[implicit_reducible]

instance Lean.Lsp.instHashableSymbolKind : Hashable SymbolKind

def Lean.Lsp.instInhabitedSymbolKind.default : SymbolKind

@[implicit_reducible]

instance Lean.Lsp.instInhabitedSymbolKind : Inhabited SymbolKind

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSymbolKind : FromJson SymbolKind

@[implicit_reducible]

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)

@[implicit_reducible]

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

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

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

@[implicit_reducible]

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

inductive Lean.Lsp.DocumentSymbol : Type

• mk (sym : DocumentSymbolAux DocumentSymbol) : DocumentSymbol

@[implicit_reducible]

instance Lean.Lsp.instToJsonDocumentSymbol : ToJson DocumentSymbol

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

structure Lean.Lsp.DocumentSymbolResult : Type

• syms : Array DocumentSymbol

@[implicit_reducible]

instance Lean.Lsp.instToJsonDocumentSymbolResult : ToJson DocumentSymbolResult

inductive Lean.Lsp.SymbolTag : Type

• deprecated : SymbolTag

@[implicit_reducible]

instance Lean.Lsp.instBEqSymbolTag : BEq SymbolTag

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

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

@[implicit_reducible]

instance Lean.Lsp.instHashableSymbolTag : Hashable SymbolTag

@[implicit_reducible]

instance Lean.Lsp.instInhabitedSymbolTag : Inhabited SymbolTag

def Lean.Lsp.instInhabitedSymbolTag.default : SymbolTag

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSymbolTag : FromJson SymbolTag

@[implicit_reducible]

instance Lean.Lsp.instToJsonSymbolTag : ToJson SymbolTag

structure Lean.Lsp.SymbolInformation : Type

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSymbolInformation : FromJson SymbolInformation

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

@[implicit_reducible]

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

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonCallHierarchyPrepareParams : FromJson CallHierarchyPrepareParams

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

@[implicit_reducible]

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

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonCallHierarchyItem : FromJson CallHierarchyItem

@[implicit_reducible]

instance Lean.Lsp.instToJsonCallHierarchyItem : ToJson CallHierarchyItem

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

@[implicit_reducible]

instance Lean.Lsp.instBEqCallHierarchyItem : BEq CallHierarchyItem

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

@[implicit_reducible]

instance Lean.Lsp.instHashableCallHierarchyItem : Hashable CallHierarchyItem

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

def Lean.Lsp.instInhabitedCallHierarchyItem.default : CallHierarchyItem

@[implicit_reducible]

instance Lean.Lsp.instInhabitedCallHierarchyItem : Inhabited CallHierarchyItem

structure Lean.Lsp.CallHierarchyIncomingCallsParams : Type

• item : CallHierarchyItem

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonCallHierarchyIncomingCallsParams : FromJson CallHierarchyIncomingCallsParams

@[implicit_reducible]

instance Lean.Lsp.instToJsonCallHierarchyIncomingCallsParams : ToJson CallHierarchyIncomingCallsParams

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

structure Lean.Lsp.CallHierarchyIncomingCall : Type

• from : CallHierarchyItem
• fromRanges : Array Range

@[implicit_reducible]

instance Lean.Lsp.instFromJsonCallHierarchyIncomingCall : FromJson CallHierarchyIncomingCall

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

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonCallHierarchyIncomingCall : ToJson CallHierarchyIncomingCall

@[implicit_reducible]

instance Lean.Lsp.instInhabitedCallHierarchyIncomingCall : Inhabited CallHierarchyIncomingCall

def Lean.Lsp.instInhabitedCallHierarchyIncomingCall.default : CallHierarchyIncomingCall

structure Lean.Lsp.CallHierarchyOutgoingCallsParams : Type

• item : CallHierarchyItem

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonCallHierarchyOutgoingCallsParams : FromJson CallHierarchyOutgoingCallsParams

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonCallHierarchyOutgoingCallsParams : ToJson CallHierarchyOutgoingCallsParams

structure Lean.Lsp.CallHierarchyOutgoingCall : Type

• to : CallHierarchyItem
• fromRanges : Array Range

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonCallHierarchyOutgoingCall : FromJson CallHierarchyOutgoingCall

@[implicit_reducible]

instance Lean.Lsp.instToJsonCallHierarchyOutgoingCall : ToJson CallHierarchyOutgoingCall

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonSemanticTokenType : ToJson SemanticTokenType

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

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSemanticTokenType : FromJson SemanticTokenType

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

@[implicit_reducible]

instance Lean.Lsp.instBEqSemanticTokenType : BEq SemanticTokenType

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

@[implicit_reducible]

instance Lean.Lsp.instHashableSemanticTokenType : Hashable SemanticTokenType

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonSemanticTokenModifier : ToJson SemanticTokenModifier

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSemanticTokensLegend : FromJson SemanticTokensLegend

@[implicit_reducible]

instance Lean.Lsp.instToJsonSemanticTokensLegend : ToJson SemanticTokensLegend

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

structure Lean.Lsp.SemanticTokensOptions : Type

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSemanticTokensOptions : FromJson SemanticTokensOptions

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSemanticTokensParams : FromJson SemanticTokensParams

@[implicit_reducible]

instance Lean.Lsp.instToJsonSemanticTokensParams : ToJson SemanticTokensParams

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

structure Lean.Lsp.SemanticTokensRangeParams : Type

• textDocument : TextDocumentIdentifier
• range : Range

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSemanticTokensRangeParams : FromJson SemanticTokensRangeParams

@[implicit_reducible]

instance Lean.Lsp.instToJsonSemanticTokensRangeParams : ToJson SemanticTokensRangeParams

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

structure Lean.Lsp.SemanticTokens : Type

• resultId? : Option String
• data : Array Nat

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSemanticTokens : FromJson SemanticTokens

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonSemanticTokens : ToJson SemanticTokens

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

structure Lean.Lsp.FoldingRangeParams : Type

• textDocument : TextDocumentIdentifier

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonFoldingRangeParams : FromJson FoldingRangeParams

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonFoldingRangeParams : ToJson FoldingRangeParams

inductive Lean.Lsp.FoldingRangeKind : Type

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonFoldingRangeKind : ToJson FoldingRangeKind

structure Lean.Lsp.FoldingRange : Type

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

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonFoldingRange : ToJson FoldingRange

structure Lean.Lsp.RenameOptions : Type

• prepareProvider : Bool

@[implicit_reducible]

instance Lean.Lsp.instFromJsonRenameOptions : FromJson RenameOptions

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

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonRenameOptions : ToJson RenameOptions

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

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonRenameParams : FromJson RenameParams

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonPrepareRenameParams : FromJson PrepareRenameParams

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

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonPrepareRenameParams : ToJson PrepareRenameParams

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

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonInlayHintParams : FromJson InlayHintParams

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

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonInlayHintParams : ToJson InlayHintParams

inductive Lean.Lsp.InlayHintTooltip : Type

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonInlayHintTooltip : FromJson InlayHintTooltip

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonInlayHintLabelPart : FromJson InlayHintLabelPart

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonInlayHintLabelPart : ToJson InlayHintLabelPart

inductive Lean.Lsp.InlayHintLabel : Type

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonInlayHintLabel : FromJson InlayHintLabel

@[implicit_reducible]

instance Lean.Lsp.instToJsonInlayHintLabel : ToJson InlayHintLabel

inductive Lean.Lsp.InlayHintKind : Type

• type : InlayHintKind
• parameter : InlayHintKind

@[implicit_reducible]

instance Lean.Lsp.instFromJsonInlayHintKind : FromJson InlayHintKind

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonInlayHint : FromJson InlayHint

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonInlayHint : ToJson InlayHint

structure Lean.Lsp.InlayHintClientCapabilities : Type

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

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonInlayHintClientCapabilities : FromJson InlayHintClientCapabilities

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonInlayHintClientCapabilities : ToJson InlayHintClientCapabilities

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

• workDoneProgress : Bool
• resolveProvider? : Option Bool

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonInlayHintOptions : FromJson InlayHintOptions

@[implicit_reducible]

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonParameterInformationLabel : FromJson ParameterInformationLabel

@[implicit_reducible]

instance Lean.Lsp.instToJsonParameterInformationLabel : ToJson ParameterInformationLabel

structure Lean.Lsp.ParameterInformation : Type

• label : ParameterInformationLabel
• documentation? : Option MarkupContent

@[implicit_reducible]

instance Lean.Lsp.instFromJsonParameterInformation : FromJson ParameterInformation

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

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonParameterInformation : ToJson ParameterInformation

structure Lean.Lsp.SignatureInformation : Type

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSignatureInformation : FromJson SignatureInformation

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonSignatureInformation : ToJson SignatureInformation

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

structure Lean.Lsp.SignatureHelp : Type

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSignatureHelp : FromJson SignatureHelp

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonSignatureHelp : ToJson SignatureHelp

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

inductive Lean.Lsp.SignatureHelpTriggerKind : Type

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSignatureHelpTriggerKind : FromJson SignatureHelpTriggerKind

@[implicit_reducible]

instance Lean.Lsp.instToJsonSignatureHelpTriggerKind : ToJson SignatureHelpTriggerKind

structure Lean.Lsp.SignatureHelpContext : Type

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSignatureHelpContext : FromJson SignatureHelpContext

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

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

@[implicit_reducible]

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

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSignatureHelpParams : FromJson SignatureHelpParams

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonSignatureHelpParams : ToJson SignatureHelpParams

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

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonSignatureHelpOptions : FromJson SignatureHelpOptions

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonSignatureHelpOptions : ToJson SignatureHelpOptions

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

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

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

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDocumentColorParams : FromJson DocumentColorParams

@[implicit_reducible]

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

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonColor : FromJson Color

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonColor : ToJson Color

structure Lean.Lsp.ColorInformation : Type

• range : Range
• color : Color

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonColorInformation : FromJson ColorInformation

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

@[implicit_reducible]

instance Lean.Lsp.instToJsonColorInformation : ToJson ColorInformation

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

• workDoneProgress : Bool

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

@[implicit_reducible]

instance Lean.Lsp.instFromJsonDocumentColorOptions : FromJson DocumentColorOptions

@[implicit_reducible]

instance Lean.Lsp.instToJsonDocumentColorOptions : ToJson DocumentColorOptions

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