structure Lean.Lsp.CompletionOptions : Type

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

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

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

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

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

• deprecated : CompletionItemTag

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

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

• isIncomplete : Bool
• items : Array CompletionItem

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

• textDocument : TextDocumentIdentifier
• position : Position

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

• contents : MarkupContent
• range? : Option Range

instance Lean.Lsp.instToJsonHover : ToJson Hover

Equations

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

instance Lean.Lsp.instFromJsonHover : FromJson Hover

Equations

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

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

• textDocument : TextDocumentIdentifier
• position : Position

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

• textDocument : TextDocumentIdentifier
• position : Position

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

• textDocument : TextDocumentIdentifier
• position : Position

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

• textDocument : TextDocumentIdentifier
• position : Position

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

• includeDeclaration : Bool

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

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

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

• query : String

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

• textDocument : TextDocumentIdentifier
• position : Position

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

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

instance Lean.Lsp.instToJsonDocumentHighlightKind : ToJson DocumentHighlightKind

Equations

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

structure Lean.Lsp.DocumentHighlight : Type

• range : Range
• kind? : Option DocumentHighlightKind

instance Lean.Lsp.instToJsonDocumentHighlight : ToJson DocumentHighlight

Equations

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

@[reducible, inline]

abbrev Lean.Lsp.DocumentHighlightResult : Type

Equations

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

structure Lean.Lsp.DocumentSymbolParams : Type

• textDocument : TextDocumentIdentifier

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

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

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

• mk (sym : DocumentSymbolAux DocumentSymbol) : DocumentSymbol

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

• syms : Array DocumentSymbol

instance Lean.Lsp.instToJsonDocumentSymbolResult : ToJson DocumentSymbolResult

Equations

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

inductive Lean.Lsp.SymbolTag : Type

• deprecated : SymbolTag

instance Lean.Lsp.instBEqSymbolTag : BEq SymbolTag

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

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

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

• textDocument : TextDocumentIdentifier
• position : Position

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

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

• item : CallHierarchyItem

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

• from : CallHierarchyItem
• fromRanges : Array Range

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

• item : CallHierarchyItem

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

• to : CallHierarchyItem
• fromRanges : Array Range

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

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 : Array String

Equations

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

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

Equations

• tokenType.toNat = tokenType.toCtorIdx

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

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 : Array String

Equations

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

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

Equations

• modifier.toNat = modifier.toCtorIdx

structure Lean.Lsp.SemanticTokensLegend : Type

• tokenTypes : Array String
• tokenModifiers : Array String

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

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

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

• textDocument : TextDocumentIdentifier

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

• textDocument : TextDocumentIdentifier
• range : Range

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

• resultId? : Option String
• data : Array Nat

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

• textDocument : TextDocumentIdentifier

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

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

instance Lean.Lsp.instToJsonFoldingRangeKind : ToJson FoldingRangeKind

Equations

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

structure Lean.Lsp.FoldingRange : Type

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

instance Lean.Lsp.instToJsonFoldingRange : ToJson FoldingRange

Equations

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

structure Lean.Lsp.RenameOptions : Type

• prepareProvider : Bool

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

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

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

• textDocument : TextDocumentIdentifier
• position : Position

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

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

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

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

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

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

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

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

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

• type : InlayHintKind
• parameter : InlayHintKind

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

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

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

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

• workDoneProgress : Bool
• resolveProvider? : Option Bool

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