structure Lean.Lsp.CompletionOptions : Type

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

instance Lean.Lsp.instFromJsonCompletionOptions : FromJson CompletionOptions

instance Lean.Lsp.instToJsonCompletionOptions : ToJson CompletionOptions

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

instance Lean.Lsp.instInhabitedCompletionItemKind : Inhabited CompletionItemKind

instance Lean.Lsp.instDecidableEqCompletionItemKind : DecidableEq CompletionItemKind

instance Lean.Lsp.instReprCompletionItemKind : Repr CompletionItemKind

instance Lean.Lsp.instHashableCompletionItemKind : Hashable CompletionItemKind

instance Lean.Lsp.instToJsonCompletionItemKind : ToJson CompletionItemKind

instance Lean.Lsp.instFromJsonCompletionItemKind : FromJson CompletionItemKind

structure Lean.Lsp.InsertReplaceEdit : Type

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

instance Lean.Lsp.instFromJsonInsertReplaceEdit : FromJson InsertReplaceEdit

instance Lean.Lsp.instToJsonInsertReplaceEdit : ToJson InsertReplaceEdit

instance Lean.Lsp.instBEqInsertReplaceEdit : BEq InsertReplaceEdit

instance Lean.Lsp.instHashableInsertReplaceEdit : Hashable InsertReplaceEdit

inductive Lean.Lsp.CompletionItemTag : Type

• deprecated : CompletionItemTag

instance Lean.Lsp.instInhabitedCompletionItemTag : Inhabited CompletionItemTag

instance Lean.Lsp.instDecidableEqCompletionItemTag : DecidableEq CompletionItemTag

instance Lean.Lsp.instReprCompletionItemTag : Repr CompletionItemTag

instance Lean.Lsp.instHashableCompletionItemTag : Hashable CompletionItemTag

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)

instance Lean.Lsp.instFromJsonCompletionItem : FromJson CompletionItem

instance Lean.Lsp.instToJsonCompletionItem : ToJson CompletionItem

instance Lean.Lsp.instInhabitedCompletionItem : Inhabited CompletionItem

instance Lean.Lsp.instBEqCompletionItem : BEq CompletionItem

instance Lean.Lsp.instHashableCompletionItem : Hashable CompletionItem

structure Lean.Lsp.CompletionList : Type

• isIncomplete : Bool
• items : Array CompletionItem

instance Lean.Lsp.instFromJsonCompletionList : FromJson CompletionList

instance Lean.Lsp.instToJsonCompletionList : ToJson CompletionList

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

• textDocument : TextDocumentIdentifier
• position : Position

instance Lean.Lsp.instFromJsonCompletionParams : FromJson CompletionParams

instance Lean.Lsp.instToJsonCompletionParams : ToJson CompletionParams

structure Lean.Lsp.Hover : Type

• contents : MarkupContent
• range? : Option Range

instance Lean.Lsp.instToJsonHover : ToJson Hover

instance Lean.Lsp.instFromJsonHover : FromJson Hover

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

• textDocument : TextDocumentIdentifier
• position : Position

instance Lean.Lsp.instFromJsonHoverParams : FromJson HoverParams

instance Lean.Lsp.instToJsonHoverParams : ToJson HoverParams

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

• textDocument : TextDocumentIdentifier
• position : Position

instance Lean.Lsp.instFromJsonDeclarationParams : FromJson DeclarationParams

instance Lean.Lsp.instToJsonDeclarationParams : ToJson DeclarationParams

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

• textDocument : TextDocumentIdentifier
• position : Position

instance Lean.Lsp.instFromJsonDefinitionParams : FromJson DefinitionParams

instance Lean.Lsp.instToJsonDefinitionParams : ToJson DefinitionParams

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

• textDocument : TextDocumentIdentifier
• position : Position

instance Lean.Lsp.instFromJsonTypeDefinitionParams : FromJson TypeDefinitionParams

instance Lean.Lsp.instToJsonTypeDefinitionParams : ToJson TypeDefinitionParams

structure Lean.Lsp.ReferenceContext : Type

• includeDeclaration : Bool

instance Lean.Lsp.instFromJsonReferenceContext : FromJson ReferenceContext

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

instance Lean.Lsp.instToJsonReferenceParams : ToJson ReferenceParams

structure Lean.Lsp.WorkspaceSymbolParams : Type

• query : String

instance Lean.Lsp.instFromJsonWorkspaceSymbolParams : FromJson WorkspaceSymbolParams

instance Lean.Lsp.instToJsonWorkspaceSymbolParams : ToJson WorkspaceSymbolParams

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

• textDocument : TextDocumentIdentifier
• position : Position

instance Lean.Lsp.instFromJsonDocumentHighlightParams : FromJson DocumentHighlightParams

instance Lean.Lsp.instToJsonDocumentHighlightParams : ToJson DocumentHighlightParams

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

@[reducible, inline]

abbrev Lean.Lsp.DocumentHighlightResult : Type

structure Lean.Lsp.DocumentSymbolParams : Type

• textDocument : TextDocumentIdentifier

instance Lean.Lsp.instFromJsonDocumentSymbolParams : FromJson DocumentSymbolParams

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

instance Lean.Lsp.instBEqSymbolKind : BEq SymbolKind

instance Lean.Lsp.instHashableSymbolKind : Hashable 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)

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

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

instance Lean.Lsp.instBEqSymbolTag : BEq SymbolTag

instance Lean.Lsp.instHashableSymbolTag : Hashable SymbolTag

instance Lean.Lsp.instInhabitedSymbolTag : Inhabited 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

instance Lean.Lsp.instFromJsonSymbolInformation : FromJson SymbolInformation

instance Lean.Lsp.instToJsonSymbolInformation : ToJson SymbolInformation

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

• textDocument : TextDocumentIdentifier
• position : Position

instance Lean.Lsp.instFromJsonCallHierarchyPrepareParams : FromJson CallHierarchyPrepareParams

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

instance Lean.Lsp.instToJsonCallHierarchyItem : ToJson CallHierarchyItem

instance Lean.Lsp.instBEqCallHierarchyItem : BEq CallHierarchyItem

instance Lean.Lsp.instHashableCallHierarchyItem : Hashable CallHierarchyItem

instance Lean.Lsp.instInhabitedCallHierarchyItem : Inhabited CallHierarchyItem

structure Lean.Lsp.CallHierarchyIncomingCallsParams : Type

• item : CallHierarchyItem

instance Lean.Lsp.instFromJsonCallHierarchyIncomingCallsParams : FromJson CallHierarchyIncomingCallsParams

instance Lean.Lsp.instToJsonCallHierarchyIncomingCallsParams : ToJson CallHierarchyIncomingCallsParams

structure Lean.Lsp.CallHierarchyIncomingCall : Type

• from : CallHierarchyItem
• fromRanges : Array Range

instance Lean.Lsp.instFromJsonCallHierarchyIncomingCall : FromJson CallHierarchyIncomingCall

instance Lean.Lsp.instToJsonCallHierarchyIncomingCall : ToJson CallHierarchyIncomingCall

instance Lean.Lsp.instInhabitedCallHierarchyIncomingCall : Inhabited CallHierarchyIncomingCall

structure Lean.Lsp.CallHierarchyOutgoingCallsParams : Type

• item : CallHierarchyItem

instance Lean.Lsp.instFromJsonCallHierarchyOutgoingCallsParams : FromJson CallHierarchyOutgoingCallsParams

instance Lean.Lsp.instToJsonCallHierarchyOutgoingCallsParams : ToJson CallHierarchyOutgoingCallsParams

structure Lean.Lsp.CallHierarchyOutgoingCall : Type

• to : CallHierarchyItem
• fromRanges : Array Range

instance Lean.Lsp.instFromJsonCallHierarchyOutgoingCall : FromJson CallHierarchyOutgoingCall

instance Lean.Lsp.instToJsonCallHierarchyOutgoingCall : ToJson CallHierarchyOutgoingCall

instance Lean.Lsp.instInhabitedCallHierarchyOutgoingCall : Inhabited 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

instance Lean.Lsp.instFromJsonSemanticTokenType : FromJson SemanticTokenType

instance Lean.Lsp.instBEqSemanticTokenType : BEq SemanticTokenType

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

instance Lean.Lsp.instToJsonSemanticTokenModifier : ToJson SemanticTokenModifier

instance Lean.Lsp.instFromJsonSemanticTokenModifier : FromJson 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

instance Lean.Lsp.instFromJsonSemanticTokensLegend : FromJson SemanticTokensLegend

instance Lean.Lsp.instToJsonSemanticTokensLegend : ToJson SemanticTokensLegend

structure Lean.Lsp.SemanticTokensOptions : Type

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

instance Lean.Lsp.instFromJsonSemanticTokensOptions : FromJson SemanticTokensOptions

instance Lean.Lsp.instToJsonSemanticTokensOptions : ToJson SemanticTokensOptions

structure Lean.Lsp.SemanticTokensParams : Type

• textDocument : TextDocumentIdentifier

instance Lean.Lsp.instFromJsonSemanticTokensParams : FromJson SemanticTokensParams

instance Lean.Lsp.instToJsonSemanticTokensParams : ToJson SemanticTokensParams

structure Lean.Lsp.SemanticTokensRangeParams : Type

• textDocument : TextDocumentIdentifier
• range : Range

instance Lean.Lsp.instFromJsonSemanticTokensRangeParams : FromJson SemanticTokensRangeParams

instance Lean.Lsp.instToJsonSemanticTokensRangeParams : ToJson SemanticTokensRangeParams

structure Lean.Lsp.SemanticTokens : Type

• resultId? : Option String
• data : Array Nat

instance Lean.Lsp.instFromJsonSemanticTokens : FromJson SemanticTokens

instance Lean.Lsp.instToJsonSemanticTokens : ToJson SemanticTokens

structure Lean.Lsp.FoldingRangeParams : Type

• textDocument : TextDocumentIdentifier

instance Lean.Lsp.instFromJsonFoldingRangeParams : FromJson FoldingRangeParams

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

structure Lean.Lsp.RenameOptions : Type

• prepareProvider : Bool

instance Lean.Lsp.instFromJsonRenameOptions : FromJson RenameOptions

instance Lean.Lsp.instToJsonRenameOptions : ToJson RenameOptions

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

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

instance Lean.Lsp.instFromJsonRenameParams : FromJson RenameParams

instance Lean.Lsp.instToJsonRenameParams : ToJson RenameParams

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

• textDocument : TextDocumentIdentifier
• position : Position

instance Lean.Lsp.instFromJsonPrepareRenameParams : FromJson PrepareRenameParams

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

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

instance Lean.Lsp.instFromJsonInlayHintLabelPart : FromJson InlayHintLabelPart

instance Lean.Lsp.instToJsonInlayHintLabelPart : ToJson InlayHintLabelPart

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

instance Lean.Lsp.instFromJsonInlayHint : FromJson InlayHint

instance Lean.Lsp.instToJsonInlayHint : ToJson InlayHint

structure Lean.Lsp.InlayHintClientCapabilities : Type

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

instance Lean.Lsp.instFromJsonInlayHintClientCapabilities : FromJson InlayHintClientCapabilities

instance Lean.Lsp.instToJsonInlayHintClientCapabilities : ToJson InlayHintClientCapabilities

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

• workDoneProgress : Bool
• resolveProvider? : Option Bool

instance Lean.Lsp.instFromJsonInlayHintOptions : FromJson InlayHintOptions

instance Lean.Lsp.instToJsonInlayHintOptions : ToJson InlayHintOptions