structure Lean.Lsp.CompletionOptions : Type

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

Instances For

• Lean.Lsp.instFromJsonCompletionOptions
• Lean.Lsp.instToJsonCompletionOptions

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

Instances For

• Lean.Lsp.instFromJsonCompletionItemKind
• Lean.Lsp.instHashableCompletionItemKind
• Lean.Lsp.instInhabitedCompletionItemKind
• Lean.Lsp.instReprCompletionItemKind
• Lean.Lsp.instToJsonCompletionItemKind

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

Instances For

• Lean.Lsp.instBEqInsertReplaceEdit
• Lean.Lsp.instFromJsonInsertReplaceEdit
• Lean.Lsp.instHashableInsertReplaceEdit
• Lean.Lsp.instToJsonInsertReplaceEdit

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

Instances For

• Lean.Lsp.instFromJsonCompletionItemTag
• Lean.Lsp.instHashableCompletionItemTag
• Lean.Lsp.instInhabitedCompletionItemTag
• Lean.Lsp.instReprCompletionItemTag
• Lean.Lsp.instToJsonCompletionItemTag

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)

Instances For

• Lean.Lsp.instBEqCompletionItem
• Lean.Lsp.instFileSourceCompletionItem
• Lean.Lsp.instFromJsonCompletionItem
• Lean.Lsp.instHashableCompletionItem
• Lean.Lsp.instInhabitedCompletionItem
• Lean.Lsp.instToJsonCompletionItem

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

Instances For

• Lean.Lsp.instFromJsonCompletionList
• Lean.Lsp.instToJsonCompletionList

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

Instances For

• Lean.Lsp.instFileSourceCompletionParams
• Lean.Lsp.instFromJsonCompletionParams
• Lean.Lsp.instToJsonCompletionParams

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

Instances For

• Lean.Lsp.instFromJsonHover
• Lean.Lsp.instToJsonHover

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

Instances For

• Lean.Lsp.instFileSourceHoverParams
• Lean.Lsp.instFromJsonHoverParams
• Lean.Lsp.instToJsonHoverParams

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

Instances For

• Lean.Lsp.instFileSourceDeclarationParams
• Lean.Lsp.instFromJsonDeclarationParams
• Lean.Lsp.instToJsonDeclarationParams

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

Instances For

• Lean.Lsp.instFileSourceDefinitionParams
• Lean.Lsp.instFromJsonDefinitionParams
• Lean.Lsp.instToJsonDefinitionParams

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

Instances For

• Lean.Lsp.instFileSourceTypeDefinitionParams
• Lean.Lsp.instFromJsonTypeDefinitionParams
• Lean.Lsp.instToJsonTypeDefinitionParams

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

Instances For

• Lean.Lsp.instFromJsonReferenceContext
• Lean.Lsp.instToJsonReferenceContext

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

Instances For

• Lean.Lsp.instFileSourceReferenceParams
• Lean.Lsp.instFromJsonReferenceParams
• Lean.Lsp.instToJsonReferenceParams

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

Instances For

• Lean.Lsp.instFromJsonWorkspaceSymbolParams
• Lean.Lsp.instToJsonWorkspaceSymbolParams

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

Instances For

• Lean.Lsp.instFileSourceDocumentHighlightParams
• Lean.Lsp.instFromJsonDocumentHighlightParams
• Lean.Lsp.instToJsonDocumentHighlightParams

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

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

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

Equations

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

structure Lean.Lsp.DocumentSymbolParams : Type

• textDocument : TextDocumentIdentifier

Instances For

• Lean.Lsp.instFileSourceDocumentSymbolParams
• Lean.Lsp.instFromJsonDocumentSymbolParams
• Lean.Lsp.instToJsonDocumentSymbolParams

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

Instances For

• Lean.Lsp.instBEqSymbolKind
• Lean.Lsp.instFromJsonSymbolKind
• Lean.Lsp.instHashableSymbolKind
• Lean.Lsp.instInhabitedSymbolKind
• Lean.Lsp.instToJsonSymbolKind

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)

Instances For

• Lean.Lsp.instFromJsonDocumentSymbolAux
• Lean.Lsp.instToJsonDocumentSymbolAux

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

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

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

• deprecated : SymbolTag

Instances For

• Lean.Lsp.instBEqSymbolTag
• Lean.Lsp.instFromJsonSymbolTag
• Lean.Lsp.instHashableSymbolTag
• Lean.Lsp.instInhabitedSymbolTag
• Lean.Lsp.instToJsonSymbolTag

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

Instances For

• Lean.Lsp.instFromJsonSymbolInformation
• Lean.Lsp.instToJsonSymbolInformation

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

Instances For

• Lean.Lsp.instFromJsonCallHierarchyPrepareParams
• Lean.Lsp.instToJsonCallHierarchyPrepareParams

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

Instances For

• Lean.Lsp.instBEqCallHierarchyItem
• Lean.Lsp.instFromJsonCallHierarchyItem
• Lean.Lsp.instHashableCallHierarchyItem
• Lean.Lsp.instInhabitedCallHierarchyItem
• Lean.Lsp.instToJsonCallHierarchyItem

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

Instances For

• Lean.Lsp.instFromJsonCallHierarchyIncomingCallsParams
• Lean.Lsp.instToJsonCallHierarchyIncomingCallsParams

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

Instances For

• Lean.Lsp.instFromJsonCallHierarchyIncomingCall
• Lean.Lsp.instInhabitedCallHierarchyIncomingCall
• Lean.Lsp.instToJsonCallHierarchyIncomingCall

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

Instances For

• Lean.Lsp.instFromJsonCallHierarchyOutgoingCallsParams
• Lean.Lsp.instToJsonCallHierarchyOutgoingCallsParams

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

Instances For

• Lean.Lsp.instFromJsonCallHierarchyOutgoingCall
• Lean.Lsp.instInhabitedCallHierarchyOutgoingCall
• Lean.Lsp.instToJsonCallHierarchyOutgoingCall

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

Instances For

• Lean.Lsp.instBEqSemanticTokenType
• Lean.Lsp.instFromJsonSemanticTokenType
• Lean.Lsp.instHashableSemanticTokenType
• Lean.Lsp.instToJsonSemanticTokenType

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

Instances For

• Lean.Lsp.instFromJsonSemanticTokenModifier
• Lean.Lsp.instToJsonSemanticTokenModifier

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

Instances For

• Lean.Lsp.instFromJsonSemanticTokensLegend
• Lean.Lsp.instToJsonSemanticTokensLegend

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

Instances For

• Lean.Lsp.instFromJsonSemanticTokensOptions
• Lean.Lsp.instToJsonSemanticTokensOptions

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

Instances For

• Lean.Lsp.instFileSourceSemanticTokensParams
• Lean.Lsp.instFromJsonSemanticTokensParams
• Lean.Lsp.instToJsonSemanticTokensParams

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

Instances For

• Lean.Lsp.instFileSourceSemanticTokensRangeParams
• Lean.Lsp.instFromJsonSemanticTokensRangeParams
• Lean.Lsp.instToJsonSemanticTokensRangeParams

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

Instances For

• Lean.Lsp.instFromJsonSemanticTokens
• Lean.Lsp.instToJsonSemanticTokens

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

Instances For

• Lean.Lsp.instFileSourceFoldingRangeParams
• Lean.Lsp.instFromJsonFoldingRangeParams
• Lean.Lsp.instToJsonFoldingRangeParams

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

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

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

• prepareProvider : Bool

Instances For

• Lean.Lsp.instFromJsonRenameOptions
• Lean.Lsp.instToJsonRenameOptions

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

Instances For

• Lean.Lsp.instFromJsonRenameParams
• Lean.Lsp.instToJsonRenameParams

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

Instances For

• Lean.Lsp.instFromJsonPrepareRenameParams
• Lean.Lsp.instToJsonPrepareRenameParams

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

Instances For

• Lean.Lsp.instFileSourceInlayHintParams
• Lean.Lsp.instFromJsonInlayHintParams
• Lean.Lsp.instToJsonInlayHintParams

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

Instances For

• Lean.Lsp.instFromJsonInlayHintTooltip
• Lean.Lsp.instToJsonInlayHintTooltip

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

Instances For

• Lean.Lsp.instFromJsonInlayHintLabelPart
• Lean.Lsp.instToJsonInlayHintLabelPart

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

Instances For

• Lean.Lsp.instFromJsonInlayHintLabel
• Lean.Lsp.instToJsonInlayHintLabel

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

Instances For

• Lean.Lsp.instFromJsonInlayHintKind
• Lean.Lsp.instToJsonInlayHintKind

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

Instances For

• Lean.Lsp.instFromJsonInlayHint
• Lean.Lsp.instToJsonInlayHint

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

Instances For

• Lean.Lsp.instFromJsonInlayHintClientCapabilities
• Lean.Lsp.instToJsonInlayHintClientCapabilities

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

Instances For

• Lean.Lsp.instFromJsonInlayHintOptions
• Lean.Lsp.instToJsonInlayHintOptions

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