structure Lean.Lsp.CompletionOptions : Type

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

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

Equations

• Lean.Lsp.instFromJsonCompletionOptions = { fromJson? := Lean.Lsp.fromJsonCompletionOptions✝ }

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

Equations

• Lean.Lsp.instToJsonCompletionOptions = { toJson := Lean.Lsp.toJsonCompletionOptions✝ }

inductive Lean.Lsp.CompletionItemKind : Type

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

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

Equations

• Lean.Lsp.instInhabitedCompletionItemKind = { default := Lean.Lsp.CompletionItemKind.text }

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

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

Equations

• Lean.Lsp.instReprCompletionItemKind = { reprPrec := Lean.Lsp.reprCompletionItemKind✝ }

instance Lean.Lsp.instHashableCompletionItemKind : Hashable Lean.Lsp.CompletionItemKind

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

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

structure Lean.Lsp.InsertReplaceEdit : Type

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

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

Equations

• Lean.Lsp.instFromJsonInsertReplaceEdit = { fromJson? := Lean.Lsp.fromJsonInsertReplaceEdit✝ }

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

instance Lean.Lsp.instBEqInsertReplaceEdit : BEq Lean.Lsp.InsertReplaceEdit

Equations

• Lean.Lsp.instBEqInsertReplaceEdit = { beq := Lean.Lsp.beqInsertReplaceEdit✝ }

instance Lean.Lsp.instHashableInsertReplaceEdit : Hashable Lean.Lsp.InsertReplaceEdit

inductive Lean.Lsp.CompletionItemTag : Type

• deprecated: Lean.Lsp.CompletionItemTag

instance Lean.Lsp.instInhabitedCompletionItemTag : Inhabited Lean.Lsp.CompletionItemTag

instance Lean.Lsp.instDecidableEqCompletionItemTag : DecidableEq Lean.Lsp.CompletionItemTag

Equations

• Lean.Lsp.instDecidableEqCompletionItemTag x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Lean.Lsp.instReprCompletionItemTag : Repr Lean.Lsp.CompletionItemTag

instance Lean.Lsp.instHashableCompletionItemTag : Hashable Lean.Lsp.CompletionItemTag

Equations

• Lean.Lsp.instHashableCompletionItemTag = { hash := Lean.Lsp.hashCompletionItemTag✝ }

instance Lean.Lsp.instToJsonCompletionItemTag : Lean.ToJson Lean.Lsp.CompletionItemTag

Equations

• Lean.Lsp.instToJsonCompletionItemTag = { toJson := fun (t : Lean.Lsp.CompletionItemTag) => Lean.toJson (t.toCtorIdx + 1) }

instance Lean.Lsp.instFromJsonCompletionItemTag : Lean.FromJson Lean.Lsp.CompletionItemTag

structure Lean.Lsp.CompletionItem : Type

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

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

Equations

• Lean.Lsp.instFromJsonCompletionItem = { fromJson? := Lean.Lsp.fromJsonCompletionItem✝ }

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

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

instance Lean.Lsp.instBEqCompletionItem : BEq Lean.Lsp.CompletionItem

Equations

• Lean.Lsp.instBEqCompletionItem = { beq := Lean.Lsp.beqCompletionItem✝ }

instance Lean.Lsp.instHashableCompletionItem : Hashable Lean.Lsp.CompletionItem

Equations

• Lean.Lsp.instHashableCompletionItem = { hash := Lean.Lsp.hashCompletionItem✝ }

structure Lean.Lsp.CompletionList : Type

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

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

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

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

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

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

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

Equations

• Lean.Lsp.instToJsonCompletionParams = { toJson := Lean.Lsp.toJsonCompletionParams✝ }

structure Lean.Lsp.Hover : Type

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

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

Equations

• Lean.Lsp.instToJsonHover = { toJson := Lean.Lsp.toJsonHover✝ }

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

Equations

• Lean.Lsp.instFromJsonHover = { fromJson? := Lean.Lsp.fromJsonHover✝ }

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

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

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

Equations

• Lean.Lsp.instFromJsonHoverParams = { fromJson? := Lean.Lsp.fromJsonHoverParams✝ }

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

Equations

• Lean.Lsp.instToJsonHoverParams = { toJson := Lean.Lsp.toJsonHoverParams✝ }

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

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

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

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

Equations

• Lean.Lsp.instToJsonDeclarationParams = { toJson := Lean.Lsp.toJsonDeclarationParams✝ }

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

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

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

Equations

• Lean.Lsp.instFromJsonDefinitionParams = { fromJson? := Lean.Lsp.fromJsonDefinitionParams✝ }

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

Equations

• Lean.Lsp.instToJsonDefinitionParams = { toJson := Lean.Lsp.toJsonDefinitionParams✝ }

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

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

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

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

Equations

• Lean.Lsp.instToJsonTypeDefinitionParams = { toJson := Lean.Lsp.toJsonTypeDefinitionParams✝ }

structure Lean.Lsp.ReferenceContext : Type

• includeDeclaration : Bool

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

Equations

• Lean.Lsp.instFromJsonReferenceContext = { fromJson? := Lean.Lsp.fromJsonReferenceContext✝ }

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

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

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

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

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

structure Lean.Lsp.WorkspaceSymbolParams : Type

• query : String

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

Equations

• Lean.Lsp.instFromJsonWorkspaceSymbolParams = { fromJson? := Lean.Lsp.fromJsonWorkspaceSymbolParams✝ }

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

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

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

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

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

inductive Lean.Lsp.DocumentHighlightKind : Type

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

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

structure Lean.Lsp.DocumentHighlight : Type

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

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

Equations

• Lean.Lsp.instToJsonDocumentHighlight = { toJson := Lean.Lsp.toJsonDocumentHighlight✝ }

@[reducible, inline]

abbrev Lean.Lsp.DocumentHighlightResult : Type

structure Lean.Lsp.DocumentSymbolParams : Type

• textDocument : Lean.Lsp.TextDocumentIdentifier

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

Equations

• Lean.Lsp.instFromJsonDocumentSymbolParams = { fromJson? := Lean.Lsp.fromJsonDocumentSymbolParams✝ }

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

Equations

• Lean.Lsp.instToJsonDocumentSymbolParams = { toJson := Lean.Lsp.toJsonDocumentSymbolParams✝ }

inductive Lean.Lsp.SymbolKind : Type

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

instance Lean.Lsp.instBEqSymbolKind : BEq Lean.Lsp.SymbolKind

Equations

• Lean.Lsp.instBEqSymbolKind = { beq := Lean.Lsp.beqSymbolKind✝ }

instance Lean.Lsp.instHashableSymbolKind : Hashable Lean.Lsp.SymbolKind

instance Lean.Lsp.instInhabitedSymbolKind : Inhabited Lean.Lsp.SymbolKind

instance Lean.Lsp.instFromJsonSymbolKind : Lean.FromJson Lean.Lsp.SymbolKind

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

Equations

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

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

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

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

Equations

• Lean.Lsp.instFromJsonDocumentSymbolAux = { fromJson? := Lean.Lsp.fromJsonDocumentSymbolAux✝ }

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

inductive Lean.Lsp.DocumentSymbol : Type

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

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

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

structure Lean.Lsp.DocumentSymbolResult : Type

• syms : Array Lean.Lsp.DocumentSymbol

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

Equations

• Lean.Lsp.instToJsonDocumentSymbolResult = { toJson := fun (dsr : Lean.Lsp.DocumentSymbolResult) => Lean.toJson dsr.syms }

inductive Lean.Lsp.SymbolTag : Type

• deprecated: Lean.Lsp.SymbolTag

instance Lean.Lsp.instBEqSymbolTag : BEq Lean.Lsp.SymbolTag

Equations

• Lean.Lsp.instBEqSymbolTag = { beq := Lean.Lsp.beqSymbolTag✝ }

instance Lean.Lsp.instHashableSymbolTag : Hashable Lean.Lsp.SymbolTag

instance Lean.Lsp.instInhabitedSymbolTag : Inhabited Lean.Lsp.SymbolTag

instance Lean.Lsp.instFromJsonSymbolTag : Lean.FromJson Lean.Lsp.SymbolTag

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

Equations

• Lean.Lsp.instToJsonSymbolTag = { toJson := fun (x : Lean.Lsp.SymbolTag) => match x with | Lean.Lsp.SymbolTag.deprecated => 1 }

structure Lean.Lsp.SymbolInformation : Type

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

instance Lean.Lsp.instFromJsonSymbolInformation : Lean.FromJson Lean.Lsp.SymbolInformation

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

Equations

• Lean.Lsp.instToJsonSymbolInformation = { toJson := Lean.Lsp.toJsonSymbolInformation✝ }

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

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

instance Lean.Lsp.instFromJsonCallHierarchyPrepareParams : Lean.FromJson Lean.Lsp.CallHierarchyPrepareParams

instance Lean.Lsp.instToJsonCallHierarchyPrepareParams : Lean.ToJson Lean.Lsp.CallHierarchyPrepareParams

Equations

• Lean.Lsp.instToJsonCallHierarchyPrepareParams = { toJson := Lean.Lsp.toJsonCallHierarchyPrepareParams✝ }

structure Lean.Lsp.CallHierarchyItem : Type

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

instance Lean.Lsp.instFromJsonCallHierarchyItem : Lean.FromJson Lean.Lsp.CallHierarchyItem

Equations

• Lean.Lsp.instFromJsonCallHierarchyItem = { fromJson? := Lean.Lsp.fromJsonCallHierarchyItem✝ }

instance Lean.Lsp.instToJsonCallHierarchyItem : Lean.ToJson Lean.Lsp.CallHierarchyItem

Equations

• Lean.Lsp.instToJsonCallHierarchyItem = { toJson := Lean.Lsp.toJsonCallHierarchyItem✝ }

instance Lean.Lsp.instBEqCallHierarchyItem : BEq Lean.Lsp.CallHierarchyItem

instance Lean.Lsp.instHashableCallHierarchyItem : Hashable Lean.Lsp.CallHierarchyItem

Equations

• Lean.Lsp.instHashableCallHierarchyItem = { hash := Lean.Lsp.hashCallHierarchyItem✝ }

instance Lean.Lsp.instInhabitedCallHierarchyItem : Inhabited Lean.Lsp.CallHierarchyItem

structure Lean.Lsp.CallHierarchyIncomingCallsParams : Type

• item : Lean.Lsp.CallHierarchyItem

instance Lean.Lsp.instFromJsonCallHierarchyIncomingCallsParams : Lean.FromJson Lean.Lsp.CallHierarchyIncomingCallsParams

instance Lean.Lsp.instToJsonCallHierarchyIncomingCallsParams : Lean.ToJson Lean.Lsp.CallHierarchyIncomingCallsParams

structure Lean.Lsp.CallHierarchyIncomingCall : Type

• from : Lean.Lsp.CallHierarchyItem
• fromRanges : Array Lean.Lsp.Range

instance Lean.Lsp.instFromJsonCallHierarchyIncomingCall : Lean.FromJson Lean.Lsp.CallHierarchyIncomingCall

instance Lean.Lsp.instToJsonCallHierarchyIncomingCall : Lean.ToJson Lean.Lsp.CallHierarchyIncomingCall

Equations

• Lean.Lsp.instToJsonCallHierarchyIncomingCall = { toJson := Lean.Lsp.toJsonCallHierarchyIncomingCall✝ }

instance Lean.Lsp.instInhabitedCallHierarchyIncomingCall : Inhabited Lean.Lsp.CallHierarchyIncomingCall

structure Lean.Lsp.CallHierarchyOutgoingCallsParams : Type

• item : Lean.Lsp.CallHierarchyItem

instance Lean.Lsp.instFromJsonCallHierarchyOutgoingCallsParams : Lean.FromJson Lean.Lsp.CallHierarchyOutgoingCallsParams

instance Lean.Lsp.instToJsonCallHierarchyOutgoingCallsParams : Lean.ToJson Lean.Lsp.CallHierarchyOutgoingCallsParams

Equations

• Lean.Lsp.instToJsonCallHierarchyOutgoingCallsParams = { toJson := Lean.Lsp.toJsonCallHierarchyOutgoingCallsParams✝ }

structure Lean.Lsp.CallHierarchyOutgoingCall : Type

• to : Lean.Lsp.CallHierarchyItem
• fromRanges : Array Lean.Lsp.Range

instance Lean.Lsp.instFromJsonCallHierarchyOutgoingCall : Lean.FromJson Lean.Lsp.CallHierarchyOutgoingCall

Equations

• Lean.Lsp.instFromJsonCallHierarchyOutgoingCall = { fromJson? := Lean.Lsp.fromJsonCallHierarchyOutgoingCall✝ }

instance Lean.Lsp.instToJsonCallHierarchyOutgoingCall : Lean.ToJson Lean.Lsp.CallHierarchyOutgoingCall

Equations

• Lean.Lsp.instToJsonCallHierarchyOutgoingCall = { toJson := Lean.Lsp.toJsonCallHierarchyOutgoingCall✝ }

instance Lean.Lsp.instInhabitedCallHierarchyOutgoingCall : Inhabited Lean.Lsp.CallHierarchyOutgoingCall

inductive Lean.Lsp.SemanticTokenType : Type

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

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

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

instance Lean.Lsp.instBEqSemanticTokenType : BEq Lean.Lsp.SemanticTokenType

Equations

• Lean.Lsp.instBEqSemanticTokenType = { beq := Lean.Lsp.beqSemanticTokenType✝ }

instance Lean.Lsp.instHashableSemanticTokenType : Hashable Lean.Lsp.SemanticTokenType

Equations

• Lean.Lsp.instHashableSemanticTokenType = { hash := Lean.Lsp.hashSemanticTokenType✝ }

def Lean.Lsp.SemanticTokenType.names : Array String

def Lean.Lsp.SemanticTokenType.toNat (tokenType : Lean.Lsp.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: Lean.Lsp.SemanticTokenModifier
• definition: Lean.Lsp.SemanticTokenModifier
• readonly: Lean.Lsp.SemanticTokenModifier
• static: Lean.Lsp.SemanticTokenModifier
• deprecated: Lean.Lsp.SemanticTokenModifier
• abstract: Lean.Lsp.SemanticTokenModifier
• async: Lean.Lsp.SemanticTokenModifier
• modification: Lean.Lsp.SemanticTokenModifier
• documentation: Lean.Lsp.SemanticTokenModifier
• defaultLibrary: Lean.Lsp.SemanticTokenModifier

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

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

def Lean.Lsp.SemanticTokenModifier.names : Array String

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

structure Lean.Lsp.SemanticTokensLegend : Type

• tokenTypes : Array String
• tokenModifiers : Array String

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

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

Equations

• Lean.Lsp.instToJsonSemanticTokensLegend = { toJson := Lean.Lsp.toJsonSemanticTokensLegend✝ }

structure Lean.Lsp.SemanticTokensOptions : Type

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

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

Equations

• Lean.Lsp.instFromJsonSemanticTokensOptions = { fromJson? := Lean.Lsp.fromJsonSemanticTokensOptions✝ }

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

Equations

• Lean.Lsp.instToJsonSemanticTokensOptions = { toJson := Lean.Lsp.toJsonSemanticTokensOptions✝ }

structure Lean.Lsp.SemanticTokensParams : Type

• textDocument : Lean.Lsp.TextDocumentIdentifier

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

Equations

• Lean.Lsp.instFromJsonSemanticTokensParams = { fromJson? := Lean.Lsp.fromJsonSemanticTokensParams✝ }

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

Equations

• Lean.Lsp.instToJsonSemanticTokensParams = { toJson := Lean.Lsp.toJsonSemanticTokensParams✝ }

structure Lean.Lsp.SemanticTokensRangeParams : Type

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

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

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

Equations

• Lean.Lsp.instToJsonSemanticTokensRangeParams = { toJson := Lean.Lsp.toJsonSemanticTokensRangeParams✝ }

structure Lean.Lsp.SemanticTokens : Type

• resultId? : Option String
• data : Array Nat

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

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

structure Lean.Lsp.FoldingRangeParams : Type

• textDocument : Lean.Lsp.TextDocumentIdentifier

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

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

Equations

• Lean.Lsp.instToJsonFoldingRangeParams = { toJson := Lean.Lsp.toJsonFoldingRangeParams✝ }

inductive Lean.Lsp.FoldingRangeKind : Type

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

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

structure Lean.Lsp.FoldingRange : Type

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

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

structure Lean.Lsp.RenameOptions : Type

• prepareProvider : Bool

instance Lean.Lsp.instFromJsonRenameOptions : Lean.FromJson Lean.Lsp.RenameOptions

Equations

• Lean.Lsp.instFromJsonRenameOptions = { fromJson? := Lean.Lsp.fromJsonRenameOptions✝ }

instance Lean.Lsp.instToJsonRenameOptions : Lean.ToJson Lean.Lsp.RenameOptions

Equations

• Lean.Lsp.instToJsonRenameOptions = { toJson := Lean.Lsp.toJsonRenameOptions✝ }

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

• textDocument : Lean.Lsp.TextDocumentIdentifier
• position : Lean.Lsp.Position
• newName : String

instance Lean.Lsp.instFromJsonRenameParams : Lean.FromJson Lean.Lsp.RenameParams

instance Lean.Lsp.instToJsonRenameParams : Lean.ToJson Lean.Lsp.RenameParams

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

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

instance Lean.Lsp.instFromJsonPrepareRenameParams : Lean.FromJson Lean.Lsp.PrepareRenameParams

Equations

• Lean.Lsp.instFromJsonPrepareRenameParams = { fromJson? := Lean.Lsp.fromJsonPrepareRenameParams✝ }

instance Lean.Lsp.instToJsonPrepareRenameParams : Lean.ToJson Lean.Lsp.PrepareRenameParams

Equations

• Lean.Lsp.instToJsonPrepareRenameParams = { toJson := Lean.Lsp.toJsonPrepareRenameParams✝ }