Lean.Data.Lsp.LanguageFeatures

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

source

structure Lean.Lsp.CompletionList:

Type

isIncomplete : Bool
items : Array Lean.Lsp.CompletionItem

source

instance Lean.Lsp.instFromJsonCompletionList:

Lean.FromJson Lean.Lsp.CompletionList

Equations

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

source

instance Lean.Lsp.instToJsonCompletionList:

Lean.ToJson Lean.Lsp.CompletionList

Equations

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

source

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

Type

source

instance Lean.Lsp.instFromJsonCompletionParams:

Lean.FromJson Lean.Lsp.CompletionParams

Equations

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

source

instance Lean.Lsp.instToJsonCompletionParams:

Lean.ToJson Lean.Lsp.CompletionParams

Equations

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

source

structure Lean.Lsp.Hover:

Type

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

source

instance Lean.Lsp.instToJsonHover:

Lean.ToJson Lean.Lsp.Hover

Equations

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

source

instance Lean.Lsp.instFromJsonHover:

Lean.FromJson Lean.Lsp.Hover

Equations

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

source

structure Lean.Lsp.HoverParamsextends 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.DeclarationParamsextends 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.DefinitionParamsextends Lean.Lsp.TextDocumentPositionParams :

Type

source

instance Lean.Lsp.instFromJsonDefinitionParams:

Lean.FromJson Lean.Lsp.DefinitionParams

Equations

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

source

instance Lean.Lsp.instToJsonDefinitionParams:

Lean.ToJson Lean.Lsp.DefinitionParams

Equations

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

source

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

Type

source

instance Lean.Lsp.instFromJsonTypeDefinitionParams:

Lean.FromJson Lean.Lsp.TypeDefinitionParams

Equations

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

source

instance Lean.Lsp.instToJsonTypeDefinitionParams:

Lean.ToJson Lean.Lsp.TypeDefinitionParams

Equations

Lean.Lsp.instToJsonTypeDefinitionParams = { toJson := [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.ReferenceParamsextends 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.instFromJsonWorkspaceSymbolParams:

Lean.FromJson Lean.Lsp.WorkspaceSymbolParams

Equations

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

source

instance Lean.Lsp.instToJsonWorkspaceSymbolParams:

Lean.ToJson Lean.Lsp.WorkspaceSymbolParams

Equations

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

source

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

Type

source

instance Lean.Lsp.instFromJsonDocumentHighlightParams:

Lean.FromJson Lean.Lsp.DocumentHighlightParams

Equations

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

source

instance Lean.Lsp.instToJsonDocumentHighlightParams:

Lean.ToJson Lean.Lsp.DocumentHighlightParams

Equations

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

source

inductive Lean.Lsp.DocumentHighlightKind:

Type

source

instance Lean.Lsp.instToJsonDocumentHighlightKind:

Lean.ToJson Lean.Lsp.DocumentHighlightKind

Equations

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

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

Lean.FromJson Lean.Lsp.DocumentSymbolParams

Equations

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

source

instance Lean.Lsp.instToJsonDocumentSymbolParams:

Lean.ToJson Lean.Lsp.DocumentSymbolParams

Equations

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

source

inductive Lean.Lsp.SymbolKind:

Type

source

instance Lean.Lsp.instToJsonSymbolKind:

Lean.ToJson Lean.Lsp.SymbolKind

Equations

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

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 := 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", "function"]

source

def Lean.Lsp.SemanticTokenType.toNat:

Lean.Lsp.SemanticTokenType → Nat

Equations

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

source

structure Lean.Lsp.SemanticTokensLegend:

Type

tokenTypes : Array String
tokenModifiers : Array String

source

instance Lean.Lsp.instFromJsonSemanticTokensLegend:

Lean.FromJson Lean.Lsp.SemanticTokensLegend

Equations

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

source

instance Lean.Lsp.instToJsonSemanticTokensLegend:

Lean.ToJson Lean.Lsp.SemanticTokensLegend

Equations

Lean.Lsp.instToJsonSemanticTokensLegend = { toJson := [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] }

source

structure Lean.Lsp.FoldingRangeParams:

Type

textDocument : Lean.Lsp.TextDocumentIdentifier

source

instance Lean.Lsp.instFromJsonFoldingRangeParams:

Lean.FromJson Lean.Lsp.FoldingRangeParams

Equations

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

source

instance Lean.Lsp.instToJsonFoldingRangeParams:

Lean.ToJson Lean.Lsp.FoldingRangeParams

Equations

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

source

inductive Lean.Lsp.FoldingRangeKind:

Type

source

instance Lean.Lsp.instToJsonFoldingRangeKind:

Lean.ToJson Lean.Lsp.FoldingRangeKind

Equations

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

source

structure Lean.Lsp.FoldingRange:

Type

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

source

instance Lean.Lsp.instToJsonFoldingRange:

Lean.ToJson Lean.Lsp.FoldingRange

Equations

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