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 :

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 :

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

Instances For

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

Equations

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

instance Lean.Lsp.instReprCompletionItemKind :

Repr Lean.Lsp.CompletionItemKind

Equations

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

instance Lean.Lsp.instHashableCompletionItemKind :

Hashable Lean.Lsp.CompletionItemKind

Equations

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

instance Lean.Lsp.instToJsonCompletionItemKind :

Lean.ToJson Lean.Lsp.CompletionItemKind

Equations

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

instance Lean.Lsp.instFromJsonCompletionItemKind :

Lean.FromJson Lean.Lsp.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 : Lean.Lsp.Range
replace : Lean.Lsp.Range

Instances For

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

Equations

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

instance Lean.Lsp.instBEqInsertReplaceEdit :

BEq Lean.Lsp.InsertReplaceEdit

Equations

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

instance Lean.Lsp.instHashableInsertReplaceEdit :

Hashable Lean.Lsp.InsertReplaceEdit

Equations

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

inductive Lean.Lsp.CompletionItemTag :

deprecated : Lean.Lsp.CompletionItemTag

Instances For

instance Lean.Lsp.instInhabitedCompletionItemTag :

Inhabited Lean.Lsp.CompletionItemTag

Equations

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

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

Equations

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

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

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 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)

Instances For

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

Equations

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

instance Lean.Lsp.instInhabitedCompletionItem :

Inhabited Lean.Lsp.CompletionItem

Equations

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

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 :

isIncomplete : Bool
items : Array Lean.Lsp.CompletionItem

Instances For

instance Lean.Lsp.instFromJsonCompletionList :

Lean.FromJson Lean.Lsp.CompletionList

Equations

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

instance Lean.Lsp.instToJsonCompletionList :

Lean.ToJson Lean.Lsp.CompletionList

Equations

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

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

Instances For

instance Lean.Lsp.instFromJsonCompletionParams :

Lean.FromJson Lean.Lsp.CompletionParams

Equations

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

instance Lean.Lsp.instToJsonCompletionParams :

Lean.ToJson Lean.Lsp.CompletionParams

Equations

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

structure Lean.Lsp.Hover :

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

Instances For

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 :

Instances For

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 :

Instances For

instance Lean.Lsp.instFromJsonDeclarationParams :

Lean.FromJson Lean.Lsp.DeclarationParams

Equations

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

instance Lean.Lsp.instToJsonDeclarationParams :

Lean.ToJson Lean.Lsp.DeclarationParams

Equations

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

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

Instances For

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 :

Instances For

instance Lean.Lsp.instFromJsonTypeDefinitionParams :

Lean.FromJson Lean.Lsp.TypeDefinitionParams

Equations

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

instance Lean.Lsp.instToJsonTypeDefinitionParams :

Lean.ToJson Lean.Lsp.TypeDefinitionParams

Equations

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

structure Lean.Lsp.ReferenceContext :

includeDeclaration : Bool

Instances For

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

Equations

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

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

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

Instances For

instance Lean.Lsp.instFromJsonReferenceParams :

Lean.FromJson Lean.Lsp.ReferenceParams

Equations

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

instance Lean.Lsp.instToJsonReferenceParams :

Lean.ToJson Lean.Lsp.ReferenceParams

Equations

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

structure Lean.Lsp.WorkspaceSymbolParams :

query : String

Instances For

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

Equations

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

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

Instances For

instance Lean.Lsp.instFromJsonDocumentHighlightParams :

Lean.FromJson Lean.Lsp.DocumentHighlightParams

Equations

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

instance Lean.Lsp.instToJsonDocumentHighlightParams :

Lean.ToJson Lean.Lsp.DocumentHighlightParams

Equations

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

inductive Lean.Lsp.DocumentHighlightKind :

Instances For

instance Lean.Lsp.instToJsonDocumentHighlightKind :

Lean.ToJson Lean.Lsp.DocumentHighlightKind

Equations

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

structure Lean.Lsp.DocumentHighlight :

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

Instances For

instance Lean.Lsp.instToJsonDocumentHighlight :

Lean.ToJson Lean.Lsp.DocumentHighlight

Equations

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

@[reducible, inline]

abbrev Lean.Lsp.DocumentHighlightResult :

Equations

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

Instances For

structure Lean.Lsp.DocumentSymbolParams :

textDocument : Lean.Lsp.TextDocumentIdentifier

Instances For

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 :

Instances For

instance Lean.Lsp.instBEqSymbolKind :

BEq Lean.Lsp.SymbolKind

Equations

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

instance Lean.Lsp.instHashableSymbolKind :

Hashable Lean.Lsp.SymbolKind

Equations

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

instance Lean.Lsp.instInhabitedSymbolKind :

Inhabited Lean.Lsp.SymbolKind

Equations

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

instance Lean.Lsp.instFromJsonSymbolKind :

Lean.FromJson Lean.Lsp.SymbolKind

Equations

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

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) :

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

Instances For

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✝)

Equations

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

inductive Lean.Lsp.DocumentSymbol :

mk (sym : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol) : Lean.Lsp.DocumentSymbol

Instances For

instance Lean.Lsp.instToJsonDocumentSymbol :

Lean.ToJson Lean.Lsp.DocumentSymbol

Equations

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

partial def Lean.Lsp.instToJsonDocumentSymbol.go :

Lean.Lsp.DocumentSymbol → Lean.Json

structure Lean.Lsp.DocumentSymbolResult :

syms : Array Lean.Lsp.DocumentSymbol

Instances For

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 :

deprecated : Lean.Lsp.SymbolTag

Instances For

instance Lean.Lsp.instBEqSymbolTag :

BEq Lean.Lsp.SymbolTag

Equations

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

instance Lean.Lsp.instHashableSymbolTag :

Hashable Lean.Lsp.SymbolTag

Equations

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

instance Lean.Lsp.instInhabitedSymbolTag :

Inhabited Lean.Lsp.SymbolTag

Equations

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

instance Lean.Lsp.instFromJsonSymbolTag :

Lean.FromJson Lean.Lsp.SymbolTag

Equations

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

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 :

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

Instances For

instance Lean.Lsp.instFromJsonSymbolInformation :

Lean.FromJson Lean.Lsp.SymbolInformation

Equations

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

instance Lean.Lsp.instToJsonSymbolInformation :

Lean.ToJson Lean.Lsp.SymbolInformation

Equations

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

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

Instances For

instance Lean.Lsp.instFromJsonCallHierarchyPrepareParams :

Lean.FromJson Lean.Lsp.CallHierarchyPrepareParams

Equations

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

instance Lean.Lsp.instToJsonCallHierarchyPrepareParams :

Lean.ToJson Lean.Lsp.CallHierarchyPrepareParams

Equations

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

structure Lean.Lsp.CallHierarchyItem :

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

Instances For

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

Equations

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

instance Lean.Lsp.instHashableCallHierarchyItem :

Hashable Lean.Lsp.CallHierarchyItem

Equations

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

instance Lean.Lsp.instInhabitedCallHierarchyItem :

Inhabited Lean.Lsp.CallHierarchyItem

Equations

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

structure Lean.Lsp.CallHierarchyIncomingCallsParams :

item : Lean.Lsp.CallHierarchyItem

Instances For

instance Lean.Lsp.instFromJsonCallHierarchyIncomingCallsParams :

Lean.FromJson Lean.Lsp.CallHierarchyIncomingCallsParams

Equations

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

instance Lean.Lsp.instToJsonCallHierarchyIncomingCallsParams :

Lean.ToJson Lean.Lsp.CallHierarchyIncomingCallsParams

Equations

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

structure Lean.Lsp.CallHierarchyIncomingCall :

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

Instances For

instance Lean.Lsp.instFromJsonCallHierarchyIncomingCall :

Lean.FromJson Lean.Lsp.CallHierarchyIncomingCall

Equations

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

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

Equations

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

structure Lean.Lsp.CallHierarchyOutgoingCallsParams :

item : Lean.Lsp.CallHierarchyItem

Instances For

instance Lean.Lsp.instFromJsonCallHierarchyOutgoingCallsParams :

Lean.FromJson Lean.Lsp.CallHierarchyOutgoingCallsParams

Equations

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

instance Lean.Lsp.instToJsonCallHierarchyOutgoingCallsParams :

Lean.ToJson Lean.Lsp.CallHierarchyOutgoingCallsParams

Equations

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

structure Lean.Lsp.CallHierarchyOutgoingCall :

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

Instances For

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

Equations

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

inductive Lean.Lsp.SemanticTokenType :

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

Instances For

instance Lean.Lsp.instToJsonSemanticTokenType :

Lean.ToJson Lean.Lsp.SemanticTokenType

Equations

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

instance Lean.Lsp.instFromJsonSemanticTokenType :

Lean.FromJson Lean.Lsp.SemanticTokenType

Equations

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

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 :

Equations

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

Instances For

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

Equations

tokenType.toNat = tokenType.toCtorIdx

Instances For

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.

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

Instances For

instance Lean.Lsp.instToJsonSemanticTokenModifier :

Lean.ToJson Lean.Lsp.SemanticTokenModifier

Equations

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

instance Lean.Lsp.instFromJsonSemanticTokenModifier :

Lean.FromJson Lean.Lsp.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"]

Instances For

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

Equations

modifier.toNat = modifier.toCtorIdx

Instances For

structure Lean.Lsp.SemanticTokensLegend :

tokenTypes : Array String
tokenModifiers : Array String

Instances For

instance Lean.Lsp.instFromJsonSemanticTokensLegend :

Lean.FromJson Lean.Lsp.SemanticTokensLegend

Equations

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

instance Lean.Lsp.instToJsonSemanticTokensLegend :

Lean.ToJson Lean.Lsp.SemanticTokensLegend

Equations

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

structure Lean.Lsp.SemanticTokensOptions :

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

Instances For

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 :

textDocument : Lean.Lsp.TextDocumentIdentifier

Instances For

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 :

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

Instances For

instance Lean.Lsp.instFromJsonSemanticTokensRangeParams :

Lean.FromJson Lean.Lsp.SemanticTokensRangeParams

Equations

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

instance Lean.Lsp.instToJsonSemanticTokensRangeParams :

Lean.ToJson Lean.Lsp.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 :

Lean.FromJson Lean.Lsp.SemanticTokens

Equations

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

instance Lean.Lsp.instToJsonSemanticTokens :

Lean.ToJson Lean.Lsp.SemanticTokens

Equations

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

structure Lean.Lsp.FoldingRangeParams :

textDocument : Lean.Lsp.TextDocumentIdentifier

Instances For

instance Lean.Lsp.instFromJsonFoldingRangeParams :

Lean.FromJson Lean.Lsp.FoldingRangeParams

Equations

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

instance Lean.Lsp.instToJsonFoldingRangeParams :

Lean.ToJson Lean.Lsp.FoldingRangeParams

Equations

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

inductive Lean.Lsp.FoldingRangeKind :

Instances For

instance Lean.Lsp.instToJsonFoldingRangeKind :

Lean.ToJson Lean.Lsp.FoldingRangeKind

Equations

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

structure Lean.Lsp.FoldingRange :

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

Instances For

instance Lean.Lsp.instToJsonFoldingRange :

Lean.ToJson Lean.Lsp.FoldingRange

Equations

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

structure Lean.Lsp.RenameOptions :

prepareProvider : Bool

Instances For

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 :

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

Instances For

instance Lean.Lsp.instFromJsonRenameParams :

Lean.FromJson Lean.Lsp.RenameParams

Equations

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

instance Lean.Lsp.instToJsonRenameParams :

Lean.ToJson Lean.Lsp.RenameParams

Equations

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

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

Instances For

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✝ }