structure Lean.Lsp.CompletionOptions : Type

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

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

Equations

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

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

Equations

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

inductive Lean.Lsp.CompletionItemKind : Type

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

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

Equations

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

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

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

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

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

Equations

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

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

Equations

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

structure Lean.Lsp.CompletionItem : Type

• label : String
• detail? : Option String
• documentation? : Option Lean.Lsp.MarkupContent
• kind? : Option Lean.Lsp.CompletionItemKind
• textEdit? : Option Lean.Lsp.InsertReplaceEdit
• sortText? : Option String
• data? : Option Lean.Json

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.

structure Lean.Lsp.CompletionList : Type

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

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

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

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

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

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

Equations

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

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

Equations

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

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

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

• includeDeclaration : Bool

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

Equations

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

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

Equations

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

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

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

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

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

• query : String

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

Equations

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

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

Equations

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

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

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

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

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

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

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

Equations

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

@[reducible, inline]

abbrev Lean.Lsp.DocumentHighlightResult : Type

Equations

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

structure Lean.Lsp.DocumentSymbolParams : Type

• textDocument : Lean.Lsp.TextDocumentIdentifier

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

Equations

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

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

Equations

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

inductive Lean.Lsp.SymbolKind : Type

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

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

Equations

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

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

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

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

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

Equations

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

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

Equations

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

inductive Lean.Lsp.DocumentSymbol : Type

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

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

• syms : Array Lean.Lsp.DocumentSymbol

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

Equations

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

inductive Lean.Lsp.SymbolTag : Type

• deprecated: Lean.Lsp.SymbolTag

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

Equations

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

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

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

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

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

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

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

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

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

Equations

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

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

Equations

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

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

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

• item : Lean.Lsp.CallHierarchyItem

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

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

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

• item : Lean.Lsp.CallHierarchyItem

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

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

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

Equations

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

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

Equations

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

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

Equations

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

inductive Lean.Lsp.SemanticTokenType : Type

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

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

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

Equations

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

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

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

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

Equations

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

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

Equations

• modifier.toNat = modifier.toCtorIdx

structure Lean.Lsp.SemanticTokensLegend : Type

• tokenTypes : Array String
• tokenModifiers : Array String

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

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

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

Equations

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

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

Equations

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

structure Lean.Lsp.SemanticTokensParams : Type

• textDocument : Lean.Lsp.TextDocumentIdentifier

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

Equations

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

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

Equations

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

structure Lean.Lsp.SemanticTokensRangeParams : Type

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

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

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

• resultId? : Option String
• data : Array Nat

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

• textDocument : Lean.Lsp.TextDocumentIdentifier

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

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

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

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

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

Equations

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

structure Lean.Lsp.RenameOptions : Type

• prepareProvider : Bool

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

Equations

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

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

Equations

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

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

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

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

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

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