Lean.Data.Lsp.LanguageFeatures

Lean.Lsp.instInhabitedCompletionItem = { default := { label := default, detail? := default, documentation? := default, kind? := default, textEdit? := default } }

source

instance Lean.Lsp.instFromJsonCompletionItem :

Lean.FromJson Lean.Lsp.CompletionItem

Equations

Lean.Lsp.instFromJsonCompletionItem = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonCompletionItem :

Lean.ToJson Lean.Lsp.CompletionItem

Equations

Lean.Lsp.instToJsonCompletionItem = { toJson := [anonymous] }

source

structure Lean.Lsp.CompletionList :

Type

isIncomplete : Bool
items : Array Lean.Lsp.CompletionItem

source

instance Lean.Lsp.instToJsonCompletionList :

Lean.ToJson Lean.Lsp.CompletionList

Equations

Lean.Lsp.instToJsonCompletionList = { toJson := [anonymous] }

source

instance Lean.Lsp.instFromJsonCompletionList :

Lean.FromJson Lean.Lsp.CompletionList

Equations

Lean.Lsp.instFromJsonCompletionList = { fromJson? := [anonymous] }

source

structure Lean.Lsp.CompletionParams extends Lean.Lsp.TextDocumentPositionParams :

Type

source

instance Lean.Lsp.instToJsonCompletionParams :

Lean.ToJson Lean.Lsp.CompletionParams

Equations

Lean.Lsp.instToJsonCompletionParams = { toJson := [anonymous] }

source

instance Lean.Lsp.instFromJsonCompletionParams :

Lean.FromJson Lean.Lsp.CompletionParams

Equations

Lean.Lsp.instFromJsonCompletionParams = { fromJson? := [anonymous] }

source

structure Lean.Lsp.Hover :

Type

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

source

instance Lean.Lsp.instFromJsonHover :

Lean.FromJson Lean.Lsp.Hover

Equations

Lean.Lsp.instFromJsonHover = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonHover :

Lean.ToJson Lean.Lsp.Hover

Equations

Lean.Lsp.instToJsonHover = { toJson := [anonymous] }

source

structure Lean.Lsp.HoverParams extends Lean.Lsp.TextDocumentPositionParams :

Type

source

instance Lean.Lsp.instFromJsonHoverParams :

Lean.FromJson Lean.Lsp.HoverParams

Equations

Lean.Lsp.instFromJsonHoverParams = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonHoverParams :

Lean.ToJson Lean.Lsp.HoverParams

Equations

Lean.Lsp.instToJsonHoverParams = { toJson := [anonymous] }

source

structure Lean.Lsp.DeclarationParams extends Lean.Lsp.TextDocumentPositionParams :

Type

source

instance Lean.Lsp.instFromJsonDeclarationParams :

Lean.FromJson Lean.Lsp.DeclarationParams

Equations

Lean.Lsp.instFromJsonDeclarationParams = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonDeclarationParams :

Lean.ToJson Lean.Lsp.DeclarationParams

Equations

Lean.Lsp.instToJsonDeclarationParams = { toJson := [anonymous] }

source

structure Lean.Lsp.DefinitionParams extends Lean.Lsp.TextDocumentPositionParams :

Type

source

instance Lean.Lsp.instToJsonDefinitionParams :

Lean.ToJson Lean.Lsp.DefinitionParams

Equations

Lean.Lsp.instToJsonDefinitionParams = { toJson := [anonymous] }

source

instance Lean.Lsp.instFromJsonDefinitionParams :

Lean.FromJson Lean.Lsp.DefinitionParams

Equations

Lean.Lsp.instFromJsonDefinitionParams = { fromJson? := [anonymous] }

source

structure Lean.Lsp.TypeDefinitionParams extends Lean.Lsp.TextDocumentPositionParams :

Type

source

instance Lean.Lsp.instToJsonTypeDefinitionParams :

Lean.ToJson Lean.Lsp.TypeDefinitionParams

Equations

Lean.Lsp.instToJsonTypeDefinitionParams = { toJson := [anonymous] }

source

instance Lean.Lsp.instFromJsonTypeDefinitionParams :

Lean.FromJson Lean.Lsp.TypeDefinitionParams

Equations

Lean.Lsp.instFromJsonTypeDefinitionParams = { fromJson? := [anonymous] }

source

structure Lean.Lsp.ReferenceContext :

Type

includeDeclaration : Bool

source

instance Lean.Lsp.instFromJsonReferenceContext :

Lean.FromJson Lean.Lsp.ReferenceContext

Equations

Lean.Lsp.instFromJsonReferenceContext = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonReferenceContext :

Lean.ToJson Lean.Lsp.ReferenceContext

Equations

Lean.Lsp.instToJsonReferenceContext = { toJson := [anonymous] }

source

structure Lean.Lsp.ReferenceParams extends Lean.Lsp.TextDocumentPositionParams :

Type

context : Lean.Lsp.ReferenceContext

source

instance Lean.Lsp.instFromJsonReferenceParams :

Lean.FromJson Lean.Lsp.ReferenceParams

Equations

Lean.Lsp.instFromJsonReferenceParams = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonReferenceParams :

Lean.ToJson Lean.Lsp.ReferenceParams

Equations

Lean.Lsp.instToJsonReferenceParams = { toJson := [anonymous] }

source

structure Lean.Lsp.WorkspaceSymbolParams :

Type

query : String

source

instance Lean.Lsp.instToJsonWorkspaceSymbolParams :

Lean.ToJson Lean.Lsp.WorkspaceSymbolParams

Equations

Lean.Lsp.instToJsonWorkspaceSymbolParams = { toJson := [anonymous] }

source

instance Lean.Lsp.instFromJsonWorkspaceSymbolParams :

Lean.FromJson Lean.Lsp.WorkspaceSymbolParams

Equations

Lean.Lsp.instFromJsonWorkspaceSymbolParams = { fromJson? := [anonymous] }

source

structure Lean.Lsp.DocumentHighlightParams extends Lean.Lsp.TextDocumentPositionParams :

Type

source

instance Lean.Lsp.instToJsonDocumentHighlightParams :

Lean.ToJson Lean.Lsp.DocumentHighlightParams

Equations

Lean.Lsp.instToJsonDocumentHighlightParams = { toJson := [anonymous] }

source

instance Lean.Lsp.instFromJsonDocumentHighlightParams :

Lean.FromJson Lean.Lsp.DocumentHighlightParams

Equations

Lean.Lsp.instFromJsonDocumentHighlightParams = { fromJson? := [anonymous] }

source

inductive Lean.Lsp.DocumentHighlightKind :

Type

source

instance Lean.Lsp.instToJsonDocumentHighlightKind :

Lean.ToJson Lean.Lsp.DocumentHighlightKind

Equations

Lean.Lsp.instToJsonDocumentHighlightKind = { toJson := fun x => match x with | Lean.Lsp.DocumentHighlightKind.text => 1 | Lean.Lsp.DocumentHighlightKind.read => 2 | Lean.Lsp.DocumentHighlightKind.write => 3 }

source

structure Lean.Lsp.DocumentHighlight :

Type

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

source

instance Lean.Lsp.instToJsonDocumentHighlight :

Lean.ToJson Lean.Lsp.DocumentHighlight

Equations

Lean.Lsp.instToJsonDocumentHighlight = { toJson := [anonymous] }

source

@[inline]

abbrev Lean.Lsp.DocumentHighlightResult :

Type

Equations

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

source

structure Lean.Lsp.DocumentSymbolParams :

Type

textDocument : Lean.Lsp.TextDocumentIdentifier

source

instance Lean.Lsp.instToJsonDocumentSymbolParams :

Lean.ToJson Lean.Lsp.DocumentSymbolParams

Equations

Lean.Lsp.instToJsonDocumentSymbolParams = { toJson := [anonymous] }

source

instance Lean.Lsp.instFromJsonDocumentSymbolParams :

Lean.FromJson Lean.Lsp.DocumentSymbolParams

Equations

Lean.Lsp.instFromJsonDocumentSymbolParams = { fromJson? := [anonymous] }

source

inductive Lean.Lsp.SymbolKind :

Type

source

instance Lean.Lsp.instToJsonSymbolKind :

Lean.ToJson Lean.Lsp.SymbolKind

Equations

Lean.Lsp.instToJsonSymbolKind = { toJson := fun x => match x with | Lean.Lsp.SymbolKind.file => 1 | Lean.Lsp.SymbolKind.module => 2 | Lean.Lsp.SymbolKind.namespace => 3 | Lean.Lsp.SymbolKind.package => 4 | Lean.Lsp.SymbolKind.class => 5 | Lean.Lsp.SymbolKind.method => 6 | Lean.Lsp.SymbolKind.property => 7 | Lean.Lsp.SymbolKind.field => 8 | Lean.Lsp.SymbolKind.constructor => 9 | Lean.Lsp.SymbolKind.enum => 10 | Lean.Lsp.SymbolKind.interface => 11 | Lean.Lsp.SymbolKind.function => 12 | Lean.Lsp.SymbolKind.variable => 13 | Lean.Lsp.SymbolKind.constant => 14 | Lean.Lsp.SymbolKind.string => 15 | Lean.Lsp.SymbolKind.number => 16 | Lean.Lsp.SymbolKind.boolean => 17 | Lean.Lsp.SymbolKind.array => 18 | Lean.Lsp.SymbolKind.object => 19 | Lean.Lsp.SymbolKind.key => 20 | Lean.Lsp.SymbolKind.null => 21 | Lean.Lsp.SymbolKind.enumMember => 22 | Lean.Lsp.SymbolKind.struct => 23 | Lean.Lsp.SymbolKind.event => 24 | Lean.Lsp.SymbolKind.operator => 25 | Lean.Lsp.SymbolKind.typeParameter => 26 }

source

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)

source

instance Lean.Lsp.instToJsonDocumentSymbolAux :

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

Equations

Lean.Lsp.instToJsonDocumentSymbolAux = { toJson := [anonymous] }

source

inductive Lean.Lsp.DocumentSymbol :

Type

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

source

instance Lean.Lsp.instToJsonDocumentSymbol :

Lean.ToJson Lean.Lsp.DocumentSymbol

Equations

Lean.Lsp.instToJsonDocumentSymbol = { toJson := (fun go => go) Lean.Lsp.instToJsonDocumentSymbol.go }

source

partial def Lean.Lsp.instToJsonDocumentSymbol.go :

Lean.Lsp.DocumentSymbol → Lean.Json

source

structure Lean.Lsp.DocumentSymbolResult :

Type

syms : Array Lean.Lsp.DocumentSymbol

source

instance Lean.Lsp.instToJsonDocumentSymbolResult :

Lean.ToJson Lean.Lsp.DocumentSymbolResult

Equations

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

source

inductive Lean.Lsp.SymbolTag :

Type

deprecated: Lean.Lsp.SymbolTag

source

instance Lean.Lsp.instToJsonSymbolTag :

Lean.ToJson Lean.Lsp.SymbolTag

Equations

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

source

structure Lean.Lsp.SymbolInformation :

Type

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

source

instance Lean.Lsp.instToJsonSymbolInformation :

Lean.ToJson Lean.Lsp.SymbolInformation

Equations

Lean.Lsp.instToJsonSymbolInformation = { toJson := [anonymous] }

source

inductive Lean.Lsp.SemanticTokenType :

Type

source

def Lean.Lsp.SemanticTokenType.names :

Array String

Equations

Lean.Lsp.SemanticTokenType.names = #["keyword", "variable", "property"]

source

def Lean.Lsp.SemanticTokenType.toNat :

Lean.Lsp.SemanticTokenType → Nat

Equations

Lean.Lsp.SemanticTokenType.toNat x = match x with | Lean.Lsp.SemanticTokenType.keyword => 0 | Lean.Lsp.SemanticTokenType.variable => 1 | Lean.Lsp.SemanticTokenType.property => 2

source

structure Lean.Lsp.SemanticTokensLegend :

Type

tokenTypes : Array String
tokenModifiers : Array String

source

instance Lean.Lsp.instToJsonSemanticTokensLegend :

Lean.ToJson Lean.Lsp.SemanticTokensLegend

Equations

Lean.Lsp.instToJsonSemanticTokensLegend = { toJson := [anonymous] }

source

instance Lean.Lsp.instFromJsonSemanticTokensLegend :

Lean.FromJson Lean.Lsp.SemanticTokensLegend

Equations

Lean.Lsp.instFromJsonSemanticTokensLegend = { fromJson? := [anonymous] }

source

structure Lean.Lsp.SemanticTokensOptions :

Type

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

source

instance Lean.Lsp.instFromJsonSemanticTokensOptions :

Lean.FromJson Lean.Lsp.SemanticTokensOptions

Equations

Lean.Lsp.instFromJsonSemanticTokensOptions = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonSemanticTokensOptions :

Lean.ToJson Lean.Lsp.SemanticTokensOptions

Equations

Lean.Lsp.instToJsonSemanticTokensOptions = { toJson := [anonymous] }

source

structure Lean.Lsp.SemanticTokensParams :

Type

textDocument : Lean.Lsp.TextDocumentIdentifier

source

instance Lean.Lsp.instFromJsonSemanticTokensParams :

Lean.FromJson Lean.Lsp.SemanticTokensParams

Equations

Lean.Lsp.instFromJsonSemanticTokensParams = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonSemanticTokensParams :

Lean.ToJson Lean.Lsp.SemanticTokensParams

Equations

Lean.Lsp.instToJsonSemanticTokensParams = { toJson := [anonymous] }

source

structure Lean.Lsp.SemanticTokensRangeParams :

Type

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

source

instance Lean.Lsp.instFromJsonSemanticTokensRangeParams :

Lean.FromJson Lean.Lsp.SemanticTokensRangeParams

Equations

Lean.Lsp.instFromJsonSemanticTokensRangeParams = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonSemanticTokensRangeParams :

Lean.ToJson Lean.Lsp.SemanticTokensRangeParams

Equations

Lean.Lsp.instToJsonSemanticTokensRangeParams = { toJson := [anonymous] }

source

structure Lean.Lsp.SemanticTokens :

Type

data : Array Nat

source

instance Lean.Lsp.instFromJsonSemanticTokens :

Lean.FromJson Lean.Lsp.SemanticTokens

Equations

Lean.Lsp.instFromJsonSemanticTokens = { fromJson? := [anonymous] }

source

instance Lean.Lsp.instToJsonSemanticTokens :

Lean.ToJson Lean.Lsp.SemanticTokens

Equations

Lean.Lsp.instToJsonSemanticTokens = { toJson := [anonymous] }