Documentation

Lean.Data.Lsp.LanguageFeatures

structure Lean.Lsp.CompletionOptions :

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

Instances For

instance Lean.Lsp.instFromJsonCompletionOptions :

FromJson CompletionOptions

Equations

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

instance Lean.Lsp.instToJsonCompletionOptions :

ToJson CompletionOptions

Equations

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

inductive Lean.Lsp.CompletionItemKind :

Instances For

instance Lean.Lsp.instInhabitedCompletionItemKind :

Inhabited CompletionItemKind

Equations

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

instance Lean.Lsp.instDecidableEqCompletionItemKind :

DecidableEq CompletionItemKind

Equations

Lean.Lsp.instDecidableEqCompletionItemKind x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Lean.Lsp.instReprCompletionItemKind :

Repr CompletionItemKind

Equations

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

instance Lean.Lsp.instHashableCompletionItemKind :

Hashable CompletionItemKind

Equations

Lean.Lsp.instHashableCompletionItemKind = { hash := Lean.Lsp.hashCompletionItemKind✝ }

instance Lean.Lsp.instToJsonCompletionItemKind :

ToJson CompletionItemKind

Equations

Lean.Lsp.instToJsonCompletionItemKind = { toJson := fun (a : Lean.Lsp.CompletionItemKind) => Lean.toJson (a.toCtorIdx + 1) }

instance Lean.Lsp.instFromJsonCompletionItemKind :

FromJson CompletionItemKind

Equations

Lean.Lsp.instFromJsonCompletionItemKind = { fromJson? := fun (v : Lean.Json) => do let i ← Lean.fromJson? v pure (Lean.Lsp.CompletionItemKind.ofNat (i - 1)) }

structure Lean.Lsp.InsertReplaceEdit :

newText : String
insert : Range
replace : Range

Instances For

instance Lean.Lsp.instFromJsonInsertReplaceEdit :

FromJson InsertReplaceEdit

Equations

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

instance Lean.Lsp.instToJsonInsertReplaceEdit :

ToJson InsertReplaceEdit

Equations

Lean.Lsp.instToJsonInsertReplaceEdit = { toJson := Lean.Lsp.toJsonInsertReplaceEdit✝ }

instance Lean.Lsp.instBEqInsertReplaceEdit :

BEq InsertReplaceEdit

Equations

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

instance Lean.Lsp.instHashableInsertReplaceEdit :

Hashable InsertReplaceEdit

Equations

Lean.Lsp.instHashableInsertReplaceEdit = { hash := Lean.Lsp.hashInsertReplaceEdit✝ }

inductive Lean.Lsp.CompletionItemTag :

deprecated : CompletionItemTag

Instances For

instance Lean.Lsp.instInhabitedCompletionItemTag :

Inhabited CompletionItemTag

Equations

Lean.Lsp.instInhabitedCompletionItemTag = { default := Lean.Lsp.CompletionItemTag.deprecated }

instance Lean.Lsp.instDecidableEqCompletionItemTag :

DecidableEq CompletionItemTag

Equations

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

instance Lean.Lsp.instReprCompletionItemTag :

Repr CompletionItemTag

Equations

Lean.Lsp.instReprCompletionItemTag = { reprPrec := Lean.Lsp.reprCompletionItemTag✝ }

instance Lean.Lsp.instHashableCompletionItemTag :

Hashable CompletionItemTag

Equations

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

instance Lean.Lsp.instToJsonCompletionItemTag :

ToJson CompletionItemTag

Equations

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

instance Lean.Lsp.instFromJsonCompletionItemTag :

FromJson CompletionItemTag

Equations

Lean.Lsp.instFromJsonCompletionItemTag = { fromJson? := fun (v : Lean.Json) => do let i ← Lean.fromJson? v pure (Lean.Lsp.CompletionItemTag.ofNat (i - 1)) }

structure Lean.Lsp.CompletionItem :

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

Instances For

instance Lean.Lsp.instFromJsonCompletionItem :

FromJson CompletionItem

Equations

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

instance Lean.Lsp.instToJsonCompletionItem :

ToJson CompletionItem

Equations

Lean.Lsp.instToJsonCompletionItem = { toJson := Lean.Lsp.toJsonCompletionItem✝ }

instance Lean.Lsp.instInhabitedCompletionItem :

Inhabited CompletionItem

Equations

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

instance Lean.Lsp.instBEqCompletionItem :

BEq CompletionItem

Equations

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

instance Lean.Lsp.instHashableCompletionItem :

Hashable CompletionItem

Equations

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

structure Lean.Lsp.CompletionList :

isIncomplete : Bool
items : Array CompletionItem

Instances For

instance Lean.Lsp.instFromJsonCompletionList :

FromJson CompletionList

Equations

Lean.Lsp.instFromJsonCompletionList = { fromJson? := Lean.Lsp.fromJsonCompletionList✝ }

instance Lean.Lsp.instToJsonCompletionList :

ToJson CompletionList

Equations

Lean.Lsp.instToJsonCompletionList = { toJson := Lean.Lsp.toJsonCompletionList✝ }

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

Instances For

instance Lean.Lsp.instFromJsonCompletionParams :

FromJson CompletionParams

Equations

Lean.Lsp.instFromJsonCompletionParams = { fromJson? := Lean.Lsp.fromJsonCompletionParams✝ }

instance Lean.Lsp.instToJsonCompletionParams :

ToJson CompletionParams

Equations

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

structure Lean.Lsp.Hover :

contents : MarkupContent
range? : Option Range

Instances For

instance Lean.Lsp.instToJsonHover :

Equations

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

instance Lean.Lsp.instFromJsonHover :

Equations

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

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

Instances For

instance Lean.Lsp.instFromJsonHoverParams :

FromJson HoverParams

Equations

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

instance Lean.Lsp.instToJsonHoverParams :

ToJson HoverParams

Equations

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

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

Instances For

instance Lean.Lsp.instFromJsonDeclarationParams :

FromJson DeclarationParams

Equations

Lean.Lsp.instFromJsonDeclarationParams = { fromJson? := Lean.Lsp.fromJsonDeclarationParams✝ }

instance Lean.Lsp.instToJsonDeclarationParams :

ToJson DeclarationParams

Equations

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

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

Instances For

instance Lean.Lsp.instFromJsonDefinitionParams :

FromJson DefinitionParams

Equations

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

instance Lean.Lsp.instToJsonDefinitionParams :

ToJson DefinitionParams

Equations

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

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

Instances For

instance Lean.Lsp.instFromJsonTypeDefinitionParams :

FromJson TypeDefinitionParams

Equations

Lean.Lsp.instFromJsonTypeDefinitionParams = { fromJson? := Lean.Lsp.fromJsonTypeDefinitionParams✝ }

instance Lean.Lsp.instToJsonTypeDefinitionParams :

ToJson TypeDefinitionParams

Equations

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

structure Lean.Lsp.ReferenceContext :

includeDeclaration : Bool

Instances For

instance Lean.Lsp.instFromJsonReferenceContext :

FromJson ReferenceContext

Equations

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

instance Lean.Lsp.instToJsonReferenceContext :

ToJson ReferenceContext

Equations

Lean.Lsp.instToJsonReferenceContext = { toJson := Lean.Lsp.toJsonReferenceContext✝ }

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

Instances For

instance Lean.Lsp.instFromJsonReferenceParams :

FromJson ReferenceParams

Equations

Lean.Lsp.instFromJsonReferenceParams = { fromJson? := Lean.Lsp.fromJsonReferenceParams✝ }

instance Lean.Lsp.instToJsonReferenceParams :

ToJson ReferenceParams

Equations

Lean.Lsp.instToJsonReferenceParams = { toJson := Lean.Lsp.toJsonReferenceParams✝ }

structure Lean.Lsp.WorkspaceSymbolParams :

query : String

Instances For

instance Lean.Lsp.instFromJsonWorkspaceSymbolParams :

FromJson WorkspaceSymbolParams

Equations

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

instance Lean.Lsp.instToJsonWorkspaceSymbolParams :

ToJson WorkspaceSymbolParams

Equations

Lean.Lsp.instToJsonWorkspaceSymbolParams = { toJson := Lean.Lsp.toJsonWorkspaceSymbolParams✝ }

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

Instances For

instance Lean.Lsp.instFromJsonDocumentHighlightParams :

FromJson DocumentHighlightParams

Equations

Lean.Lsp.instFromJsonDocumentHighlightParams = { fromJson? := Lean.Lsp.fromJsonDocumentHighlightParams✝ }

instance Lean.Lsp.instToJsonDocumentHighlightParams :

ToJson DocumentHighlightParams

Equations

Lean.Lsp.instToJsonDocumentHighlightParams = { toJson := Lean.Lsp.toJsonDocumentHighlightParams✝ }

inductive Lean.Lsp.DocumentHighlightKind :

Instances For

Lean.Lsp.instToJsonDocumentHighlightKind

instance Lean.Lsp.instToJsonDocumentHighlightKind :

ToJson DocumentHighlightKind

Equations

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

structure Lean.Lsp.DocumentHighlight :

range : Range
kind? : Option DocumentHighlightKind

Instances For

Lean.Lsp.instToJsonDocumentHighlight

instance Lean.Lsp.instToJsonDocumentHighlight :

ToJson DocumentHighlight

Equations

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

@[reducible, inline]

abbrev Lean.Lsp.DocumentHighlightResult :

Equations

Lean.Lsp.DocumentHighlightResult = Array Lean.Lsp.DocumentHighlight

structure Lean.Lsp.DocumentSymbolParams :

textDocument : TextDocumentIdentifier

Instances For

instance Lean.Lsp.instFromJsonDocumentSymbolParams :

FromJson DocumentSymbolParams

Equations

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

instance Lean.Lsp.instToJsonDocumentSymbolParams :

ToJson DocumentSymbolParams

Equations

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

inductive Lean.Lsp.SymbolKind :

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

Instances For

instance Lean.Lsp.instBEqSymbolKind :

Equations

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

instance Lean.Lsp.instHashableSymbolKind :

Hashable SymbolKind

Equations

Lean.Lsp.instHashableSymbolKind = { hash := Lean.Lsp.hashSymbolKind✝ }

instance Lean.Lsp.instInhabitedSymbolKind :

Inhabited SymbolKind

Equations

Lean.Lsp.instInhabitedSymbolKind = { default := Lean.Lsp.SymbolKind.file }

instance Lean.Lsp.instFromJsonSymbolKind :

FromJson SymbolKind

Equations

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

instance Lean.Lsp.instToJsonSymbolKind :

ToJson SymbolKind

Equations

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

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

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

Instances For

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

FromJson (DocumentSymbolAux Self✝)

Equations

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

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

ToJson (DocumentSymbolAux Self✝)

Equations

Lean.Lsp.instToJsonDocumentSymbolAux = { toJson := Lean.Lsp.toJsonDocumentSymbolAux✝ }

inductive Lean.Lsp.DocumentSymbol :

mk (sym : DocumentSymbolAux DocumentSymbol) : DocumentSymbol

Instances For

Lean.Lsp.instToJsonDocumentSymbol

instance Lean.Lsp.instToJsonDocumentSymbol :

ToJson DocumentSymbol

Equations

Lean.Lsp.instToJsonDocumentSymbol = { toJson := Lean.Lsp.instToJsonDocumentSymbol.go }

partial def Lean.Lsp.instToJsonDocumentSymbol.go :

DocumentSymbol → Json

structure Lean.Lsp.DocumentSymbolResult :

syms : Array DocumentSymbol

Instances For

Lean.Lsp.instToJsonDocumentSymbolResult

instance Lean.Lsp.instToJsonDocumentSymbolResult :

ToJson DocumentSymbolResult

Equations

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

inductive Lean.Lsp.SymbolTag :

deprecated : SymbolTag

Instances For

instance Lean.Lsp.instBEqSymbolTag :

Equations

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

instance Lean.Lsp.instHashableSymbolTag :

Hashable SymbolTag

Equations

Lean.Lsp.instHashableSymbolTag = { hash := Lean.Lsp.hashSymbolTag✝ }

instance Lean.Lsp.instInhabitedSymbolTag :

Inhabited SymbolTag

Equations

Lean.Lsp.instInhabitedSymbolTag = { default := Lean.Lsp.SymbolTag.deprecated }

instance Lean.Lsp.instFromJsonSymbolTag :

FromJson SymbolTag

Equations

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

instance Lean.Lsp.instToJsonSymbolTag :

ToJson SymbolTag

Equations

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

structure Lean.Lsp.SymbolInformation :

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

Instances For

instance Lean.Lsp.instFromJsonSymbolInformation :

FromJson SymbolInformation

Equations

Lean.Lsp.instFromJsonSymbolInformation = { fromJson? := Lean.Lsp.fromJsonSymbolInformation✝ }

instance Lean.Lsp.instToJsonSymbolInformation :

ToJson SymbolInformation

Equations

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

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

Instances For

instance Lean.Lsp.instFromJsonCallHierarchyPrepareParams :

FromJson CallHierarchyPrepareParams

Equations

Lean.Lsp.instFromJsonCallHierarchyPrepareParams = { fromJson? := Lean.Lsp.fromJsonCallHierarchyPrepareParams✝ }

instance Lean.Lsp.instToJsonCallHierarchyPrepareParams :

ToJson CallHierarchyPrepareParams

Equations

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

structure Lean.Lsp.CallHierarchyItem :

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

Instances For

instance Lean.Lsp.instFromJsonCallHierarchyItem :

FromJson CallHierarchyItem

Equations

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

instance Lean.Lsp.instToJsonCallHierarchyItem :

ToJson CallHierarchyItem

Equations

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

instance Lean.Lsp.instBEqCallHierarchyItem :

BEq CallHierarchyItem

Equations

Lean.Lsp.instBEqCallHierarchyItem = { beq := Lean.Lsp.beqCallHierarchyItem✝ }

instance Lean.Lsp.instHashableCallHierarchyItem :

Hashable CallHierarchyItem

Equations

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

instance Lean.Lsp.instInhabitedCallHierarchyItem :

Inhabited CallHierarchyItem

Equations

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

structure Lean.Lsp.CallHierarchyIncomingCallsParams :

item : CallHierarchyItem

Instances For

instance Lean.Lsp.instFromJsonCallHierarchyIncomingCallsParams :

FromJson CallHierarchyIncomingCallsParams

Equations

Lean.Lsp.instFromJsonCallHierarchyIncomingCallsParams = { fromJson? := Lean.Lsp.fromJsonCallHierarchyIncomingCallsParams✝ }

instance Lean.Lsp.instToJsonCallHierarchyIncomingCallsParams :

ToJson CallHierarchyIncomingCallsParams

Equations

Lean.Lsp.instToJsonCallHierarchyIncomingCallsParams = { toJson := Lean.Lsp.toJsonCallHierarchyIncomingCallsParams✝ }

structure Lean.Lsp.CallHierarchyIncomingCall :

from : CallHierarchyItem
fromRanges : Array Range

Instances For

instance Lean.Lsp.instFromJsonCallHierarchyIncomingCall :

FromJson CallHierarchyIncomingCall

Equations

Lean.Lsp.instFromJsonCallHierarchyIncomingCall = { fromJson? := Lean.Lsp.fromJsonCallHierarchyIncomingCall✝ }

instance Lean.Lsp.instToJsonCallHierarchyIncomingCall :

ToJson CallHierarchyIncomingCall

Equations

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

instance Lean.Lsp.instInhabitedCallHierarchyIncomingCall :

Inhabited CallHierarchyIncomingCall

Equations

Lean.Lsp.instInhabitedCallHierarchyIncomingCall = { default := { «from» := default, fromRanges := default } }

structure Lean.Lsp.CallHierarchyOutgoingCallsParams :

item : CallHierarchyItem

Instances For

instance Lean.Lsp.instFromJsonCallHierarchyOutgoingCallsParams :

FromJson CallHierarchyOutgoingCallsParams

Equations

Lean.Lsp.instFromJsonCallHierarchyOutgoingCallsParams = { fromJson? := Lean.Lsp.fromJsonCallHierarchyOutgoingCallsParams✝ }

instance Lean.Lsp.instToJsonCallHierarchyOutgoingCallsParams :

ToJson CallHierarchyOutgoingCallsParams

Equations

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

structure Lean.Lsp.CallHierarchyOutgoingCall :

to : CallHierarchyItem
fromRanges : Array Range

Instances For

instance Lean.Lsp.instFromJsonCallHierarchyOutgoingCall :

FromJson CallHierarchyOutgoingCall

Equations

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

instance Lean.Lsp.instToJsonCallHierarchyOutgoingCall :

ToJson CallHierarchyOutgoingCall

Equations

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

instance Lean.Lsp.instInhabitedCallHierarchyOutgoingCall :

Inhabited CallHierarchyOutgoingCall

Equations

Lean.Lsp.instInhabitedCallHierarchyOutgoingCall = { default := { to := default, fromRanges := default } }

inductive Lean.Lsp.SemanticTokenType :

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

Instances For

instance Lean.Lsp.instToJsonSemanticTokenType :

ToJson SemanticTokenType

Equations

Lean.Lsp.instToJsonSemanticTokenType = { toJson := Lean.Lsp.toJsonSemanticTokenType✝ }

instance Lean.Lsp.instFromJsonSemanticTokenType :

FromJson SemanticTokenType

Equations

Lean.Lsp.instFromJsonSemanticTokenType = { fromJson? := Lean.Lsp.fromJsonSemanticTokenType✝ }

instance Lean.Lsp.instBEqSemanticTokenType :

BEq SemanticTokenType

Equations

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

instance Lean.Lsp.instHashableSemanticTokenType :

Hashable SemanticTokenType

Equations

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

def Lean.Lsp.SemanticTokenType.names :

Equations

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

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

Equations

tokenType.toNat = tokenType.toCtorIdx

inductive Lean.Lsp.SemanticTokenModifier :

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

Instances For

instance Lean.Lsp.instToJsonSemanticTokenModifier :

ToJson SemanticTokenModifier

Equations

Lean.Lsp.instToJsonSemanticTokenModifier = { toJson := Lean.Lsp.toJsonSemanticTokenModifier✝ }

instance Lean.Lsp.instFromJsonSemanticTokenModifier :

FromJson SemanticTokenModifier

Equations

Lean.Lsp.instFromJsonSemanticTokenModifier = { fromJson? := Lean.Lsp.fromJsonSemanticTokenModifier✝ }

def Lean.Lsp.SemanticTokenModifier.names :

Equations

Lean.Lsp.SemanticTokenModifier.names = #["declaration", "definition", "readonly", "static", "deprecated", "abstract", "async", "modification", "documentation", "defaultLibrary"]

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

Equations

modifier.toNat = modifier.toCtorIdx

structure Lean.Lsp.SemanticTokensLegend :

tokenTypes : Array String
tokenModifiers : Array String

Instances For

instance Lean.Lsp.instFromJsonSemanticTokensLegend :

FromJson SemanticTokensLegend

Equations

Lean.Lsp.instFromJsonSemanticTokensLegend = { fromJson? := Lean.Lsp.fromJsonSemanticTokensLegend✝ }

instance Lean.Lsp.instToJsonSemanticTokensLegend :

ToJson SemanticTokensLegend

Equations

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

structure Lean.Lsp.SemanticTokensOptions :

legend : SemanticTokensLegend
range : Bool
full : Bool

Instances For

instance Lean.Lsp.instFromJsonSemanticTokensOptions :

FromJson SemanticTokensOptions

Equations

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

instance Lean.Lsp.instToJsonSemanticTokensOptions :

ToJson SemanticTokensOptions

Equations

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

structure Lean.Lsp.SemanticTokensParams :

textDocument : TextDocumentIdentifier

Instances For

instance Lean.Lsp.instFromJsonSemanticTokensParams :

FromJson SemanticTokensParams

Equations

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

instance Lean.Lsp.instToJsonSemanticTokensParams :

ToJson SemanticTokensParams

Equations

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

structure Lean.Lsp.SemanticTokensRangeParams :

textDocument : TextDocumentIdentifier
range : Range

Instances For

instance Lean.Lsp.instFromJsonSemanticTokensRangeParams :

FromJson SemanticTokensRangeParams

Equations

Lean.Lsp.instFromJsonSemanticTokensRangeParams = { fromJson? := Lean.Lsp.fromJsonSemanticTokensRangeParams✝ }

instance Lean.Lsp.instToJsonSemanticTokensRangeParams :

ToJson SemanticTokensRangeParams

Equations

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

structure Lean.Lsp.SemanticTokens :

resultId? : Option String
data : Array Nat

Instances For

instance Lean.Lsp.instFromJsonSemanticTokens :

FromJson SemanticTokens

Equations

Lean.Lsp.instFromJsonSemanticTokens = { fromJson? := Lean.Lsp.fromJsonSemanticTokens✝ }

instance Lean.Lsp.instToJsonSemanticTokens :

ToJson SemanticTokens

Equations

Lean.Lsp.instToJsonSemanticTokens = { toJson := Lean.Lsp.toJsonSemanticTokens✝ }

structure Lean.Lsp.FoldingRangeParams :

textDocument : TextDocumentIdentifier

Instances For

instance Lean.Lsp.instFromJsonFoldingRangeParams :

FromJson FoldingRangeParams

Equations

Lean.Lsp.instFromJsonFoldingRangeParams = { fromJson? := Lean.Lsp.fromJsonFoldingRangeParams✝ }

instance Lean.Lsp.instToJsonFoldingRangeParams :

ToJson FoldingRangeParams

Equations

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

inductive Lean.Lsp.FoldingRangeKind :

Instances For

Lean.Lsp.instToJsonFoldingRangeKind

instance Lean.Lsp.instToJsonFoldingRangeKind :

ToJson FoldingRangeKind

Equations

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

structure Lean.Lsp.FoldingRange :

startLine : Nat
endLine : Nat
kind? : Option FoldingRangeKind

Instances For

Lean.Lsp.instToJsonFoldingRange

instance Lean.Lsp.instToJsonFoldingRange :

ToJson FoldingRange

Equations

Lean.Lsp.instToJsonFoldingRange = { toJson := Lean.Lsp.toJsonFoldingRange✝ }

structure Lean.Lsp.RenameOptions :

prepareProvider : Bool

Instances For

instance Lean.Lsp.instFromJsonRenameOptions :

FromJson RenameOptions

Equations

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

instance Lean.Lsp.instToJsonRenameOptions :

ToJson RenameOptions

Equations

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

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

Instances For

instance Lean.Lsp.instFromJsonRenameParams :

FromJson RenameParams

Equations

Lean.Lsp.instFromJsonRenameParams = { fromJson? := Lean.Lsp.fromJsonRenameParams✝ }

instance Lean.Lsp.instToJsonRenameParams :

ToJson RenameParams

Equations

Lean.Lsp.instToJsonRenameParams = { toJson := Lean.Lsp.toJsonRenameParams✝ }

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

Instances For

instance Lean.Lsp.instFromJsonPrepareRenameParams :

FromJson PrepareRenameParams

Equations

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

instance Lean.Lsp.instToJsonPrepareRenameParams :

ToJson PrepareRenameParams

Equations

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

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

Instances For

instance Lean.Lsp.instFromJsonInlayHintParams :

FromJson InlayHintParams

Equations

Lean.Lsp.instFromJsonInlayHintParams = { fromJson? := Lean.Lsp.fromJsonInlayHintParams✝ }

instance Lean.Lsp.instToJsonInlayHintParams :

ToJson InlayHintParams

Equations

Lean.Lsp.instToJsonInlayHintParams = { toJson := Lean.Lsp.toJsonInlayHintParams✝ }

inductive Lean.Lsp.InlayHintTooltip :

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

Instances For

instance Lean.Lsp.instFromJsonInlayHintTooltip :

FromJson InlayHintTooltip

Equations

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

instance Lean.Lsp.instToJsonInlayHintTooltip :

ToJson InlayHintTooltip

Equations

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

structure Lean.Lsp.InlayHintLabelPart :

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

Instances For

instance Lean.Lsp.instFromJsonInlayHintLabelPart :

FromJson InlayHintLabelPart

Equations

Lean.Lsp.instFromJsonInlayHintLabelPart = { fromJson? := Lean.Lsp.fromJsonInlayHintLabelPart✝ }

instance Lean.Lsp.instToJsonInlayHintLabelPart :

ToJson InlayHintLabelPart

Equations

Lean.Lsp.instToJsonInlayHintLabelPart = { toJson := Lean.Lsp.toJsonInlayHintLabelPart✝ }

inductive Lean.Lsp.InlayHintLabel :

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

Instances For

instance Lean.Lsp.instFromJsonInlayHintLabel :

FromJson InlayHintLabel

Equations

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

instance Lean.Lsp.instToJsonInlayHintLabel :

ToJson InlayHintLabel

Equations

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

inductive Lean.Lsp.InlayHintKind :

type : InlayHintKind
parameter : InlayHintKind

Instances For

instance Lean.Lsp.instFromJsonInlayHintKind :

FromJson InlayHintKind

Equations

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

instance Lean.Lsp.instToJsonInlayHintKind :

ToJson InlayHintKind

Equations

Lean.Lsp.instToJsonInlayHintKind = { toJson := fun (x : Lean.Lsp.InlayHintKind) => match x with | Lean.Lsp.InlayHintKind.type => 1 | Lean.Lsp.InlayHintKind.parameter => 2 }

structure Lean.Lsp.InlayHint :

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

Instances For

instance Lean.Lsp.instFromJsonInlayHint :

FromJson InlayHint

Equations

Lean.Lsp.instFromJsonInlayHint = { fromJson? := Lean.Lsp.fromJsonInlayHint✝ }

instance Lean.Lsp.instToJsonInlayHint :

ToJson InlayHint

Equations

Lean.Lsp.instToJsonInlayHint = { toJson := Lean.Lsp.toJsonInlayHint✝ }

structure Lean.Lsp.InlayHintClientCapabilities :

dynamicRegistration? : Option Bool
resolveSupport? : Option ResolveSupport

Instances For

instance Lean.Lsp.instFromJsonInlayHintClientCapabilities :

FromJson InlayHintClientCapabilities

Equations

Lean.Lsp.instFromJsonInlayHintClientCapabilities = { fromJson? := Lean.Lsp.fromJsonInlayHintClientCapabilities✝ }

instance Lean.Lsp.instToJsonInlayHintClientCapabilities :

ToJson InlayHintClientCapabilities

Equations

Lean.Lsp.instToJsonInlayHintClientCapabilities = { toJson := Lean.Lsp.toJsonInlayHintClientCapabilities✝ }

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

workDoneProgress : Bool
resolveProvider? : Option Bool

Instances For

instance Lean.Lsp.instFromJsonInlayHintOptions :

FromJson InlayHintOptions

Equations

Lean.Lsp.instFromJsonInlayHintOptions = { fromJson? := Lean.Lsp.fromJsonInlayHintOptions✝ }

instance Lean.Lsp.instToJsonInlayHintOptions :

ToJson InlayHintOptions

Equations

Lean.Lsp.instToJsonInlayHintOptions = { toJson := Lean.Lsp.toJsonInlayHintOptions✝ }