Defines most of the 'Basic Structures' in the LSP specification (https://microsoft.github.io/language-server-protocol/specifications/specification-current/), as well as some utilities.

Since LSP is Json-based, Ints/Nats are represented by Floats on the wire.

structure Lean.Lsp.CancelParams : Type

• id : Lean.JsonRpc.RequestID

instance Lean.Lsp.instInhabitedCancelParams : Inhabited Lean.Lsp.CancelParams

Equations

• Lean.Lsp.instInhabitedCancelParams = { default := { id := default } }

instance Lean.Lsp.instBEqCancelParams : BEq Lean.Lsp.CancelParams

Equations

• Lean.Lsp.instBEqCancelParams = { beq := Lean.Lsp.beqCancelParams✝ }

instance Lean.Lsp.instToJsonCancelParams : Lean.ToJson Lean.Lsp.CancelParams

Equations

• Lean.Lsp.instToJsonCancelParams = { toJson := Lean.Lsp.toJsonCancelParams✝ }

instance Lean.Lsp.instFromJsonCancelParams : Lean.FromJson Lean.Lsp.CancelParams

Equations

• Lean.Lsp.instFromJsonCancelParams = { fromJson? := Lean.Lsp.fromJsonCancelParams✝ }

@[inline, reducible]

abbrev Lean.Lsp.DocumentUri : Type

Equations

• Lean.Lsp.DocumentUri = String

structure Lean.Lsp.Position : Type

We adopt the convention that zero-based UTF-16 positions as sent by LSP clients are represented by Lsp.Position while internally we mostly use String.Pos UTF-8 offsets. For diagnostics, one-based Lean.Positions are used internally. character is accepted liberally: actual character := min(line length, character)

• line : Nat
• character : Nat

instance Lean.Lsp.instInhabitedPosition : Inhabited Lean.Lsp.Position

Equations

• Lean.Lsp.instInhabitedPosition = { default := { line := default, character := default } }

instance Lean.Lsp.instBEqPosition : BEq Lean.Lsp.Position

Equations

• Lean.Lsp.instBEqPosition = { beq := Lean.Lsp.beqPosition✝ }

instance Lean.Lsp.instOrdPosition : Ord Lean.Lsp.Position

Equations

• Lean.Lsp.instOrdPosition = { compare := Lean.Lsp.ordPosition✝ }

instance Lean.Lsp.instHashablePosition : Hashable Lean.Lsp.Position

Equations

• Lean.Lsp.instHashablePosition = { hash := Lean.Lsp.hashPosition✝ }

instance Lean.Lsp.instToJsonPosition : Lean.ToJson Lean.Lsp.Position

Equations

• Lean.Lsp.instToJsonPosition = { toJson := Lean.Lsp.toJsonPosition✝ }

instance Lean.Lsp.instFromJsonPosition : Lean.FromJson Lean.Lsp.Position

Equations

• Lean.Lsp.instFromJsonPosition = { fromJson? := Lean.Lsp.fromJsonPosition✝ }

instance Lean.Lsp.instToStringPosition : ToString Lean.Lsp.Position

Equations

• Lean.Lsp.instToStringPosition = { toString := fun (p : Lean.Lsp.Position) => "(" ++ toString p.line ++ ", " ++ toString p.character ++ ")" }

instance Lean.Lsp.instLTPosition : LT Lean.Lsp.Position

Equations

• Lean.Lsp.instLTPosition = ltOfOrd

instance Lean.Lsp.instLEPosition : LE Lean.Lsp.Position

Equations

• Lean.Lsp.instLEPosition = leOfOrd

structure Lean.Lsp.Range : Type

• start : Lean.Lsp.Position
• end : Lean.Lsp.Position

instance Lean.Lsp.instInhabitedRange : Inhabited Lean.Lsp.Range

Equations

• Lean.Lsp.instInhabitedRange = { default := { start := default, end := default } }

instance Lean.Lsp.instBEqRange : BEq Lean.Lsp.Range

Equations

• Lean.Lsp.instBEqRange = { beq := Lean.Lsp.beqRange✝ }

instance Lean.Lsp.instHashableRange : Hashable Lean.Lsp.Range

Equations

• Lean.Lsp.instHashableRange = { hash := Lean.Lsp.hashRange✝ }

instance Lean.Lsp.instToJsonRange : Lean.ToJson Lean.Lsp.Range

Equations

• Lean.Lsp.instToJsonRange = { toJson := Lean.Lsp.toJsonRange✝ }

instance Lean.Lsp.instFromJsonRange : Lean.FromJson Lean.Lsp.Range

Equations

• Lean.Lsp.instFromJsonRange = { fromJson? := Lean.Lsp.fromJsonRange✝ }

instance Lean.Lsp.instOrdRange : Ord Lean.Lsp.Range

Equations

• Lean.Lsp.instOrdRange = { compare := Lean.Lsp.ordRange✝ }

instance Lean.Lsp.instLTRange : LT Lean.Lsp.Range

Equations

• Lean.Lsp.instLTRange = ltOfOrd

instance Lean.Lsp.instLERange : LE Lean.Lsp.Range

Equations

• Lean.Lsp.instLERange = leOfOrd

structure Lean.Lsp.Location : Type

A Location is a DocumentUri and a Range.

• uri : Lean.Lsp.DocumentUri
• range : Lean.Lsp.Range

instance Lean.Lsp.instInhabitedLocation : Inhabited Lean.Lsp.Location

Equations

• Lean.Lsp.instInhabitedLocation = { default := { uri := default, range := default } }

instance Lean.Lsp.instBEqLocation : BEq Lean.Lsp.Location

Equations

• Lean.Lsp.instBEqLocation = { beq := Lean.Lsp.beqLocation✝ }

instance Lean.Lsp.instToJsonLocation : Lean.ToJson Lean.Lsp.Location

Equations

• Lean.Lsp.instToJsonLocation = { toJson := Lean.Lsp.toJsonLocation✝ }

instance Lean.Lsp.instFromJsonLocation : Lean.FromJson Lean.Lsp.Location

Equations

• Lean.Lsp.instFromJsonLocation = { fromJson? := Lean.Lsp.fromJsonLocation✝ }

structure Lean.Lsp.LocationLink : Type

• originSelectionRange? : Option Lean.Lsp.Range
• targetUri : Lean.Lsp.DocumentUri
• targetRange : Lean.Lsp.Range
• targetSelectionRange : Lean.Lsp.Range

instance Lean.Lsp.instToJsonLocationLink : Lean.ToJson Lean.Lsp.LocationLink

Equations

• Lean.Lsp.instToJsonLocationLink = { toJson := Lean.Lsp.toJsonLocationLink✝ }

instance Lean.Lsp.instFromJsonLocationLink : Lean.FromJson Lean.Lsp.LocationLink

Equations

• Lean.Lsp.instFromJsonLocationLink = { fromJson? := Lean.Lsp.fromJsonLocationLink✝ }

structure Lean.Lsp.Command : Type

Represents a reference to a client editor command.

NOTE: No specific commands are specified by LSP, hence possible commands need to be announced as capabilities.

reference

• title : String

  Title of the command, like save.

• command : String

  The identifier of the actual command handler.

• arguments? : Option (Array Lean.Json)

  Arguments that the command handler should be invoked with.

instance Lean.Lsp.instToJsonCommand : Lean.ToJson Lean.Lsp.Command

Equations

• Lean.Lsp.instToJsonCommand = { toJson := Lean.Lsp.toJsonCommand✝ }

instance Lean.Lsp.instFromJsonCommand : Lean.FromJson Lean.Lsp.Command

Equations

• Lean.Lsp.instFromJsonCommand = { fromJson? := Lean.Lsp.fromJsonCommand✝ }

structure Lean.Lsp.SnippetString : Type

A snippet is a string that gets inserted into a document, and can afterwards be edited by the user in a structured way.

Snippets contain instructions that specify how this structured editing should proceed. They are expressed in a domain-specific language based on one from TextMate, including the following constructs:

• Designated positions for subsequent user input, called "tab stops" after their most frequently-used keybinding. They are denoted with $1, $2, and so forth. $0 denotes where the cursor should be positioned after all edits are completed, defaulting to the end of the string. Snippet tab stops are unrelated to tab stops used for indentation.
• Tab stops with default values, called placeholders, written ${1:default}. The default may itself contain a tab stop or a further placeholder and multiple options to select from may be provided by surrounding them with |s and separating them with ,, as in ${1|if $2 then $3 else $4,if let $2 := $3 then $4 else $5|}.
• One of a set of predefined variables that are replaced with their values. This includes the current line number ($TM_LINE_NUMBER) or the text that was selected when the snippet was invoked ($TM_SELECTED_TEXT).
• Formatting instructions to modify variables using regular expressions or a set of predefined filters.

The full syntax and semantics of snippets, including the available variables and the rules for escaping control characters, are described in the LSP specification.

• value : String

instance Lean.Lsp.instToJsonSnippetString : Lean.ToJson Lean.Lsp.SnippetString

Equations

• Lean.Lsp.instToJsonSnippetString = { toJson := Lean.Lsp.toJsonSnippetString✝ }

instance Lean.Lsp.instFromJsonSnippetString : Lean.FromJson Lean.Lsp.SnippetString

Equations

• Lean.Lsp.instFromJsonSnippetString = { fromJson? := Lean.Lsp.fromJsonSnippetString✝ }

structure Lean.Lsp.TextEdit : Type

A textual edit applicable to a text document.

reference

• range : Lean.Lsp.Range

  The range of the text document to be manipulated. To insert text into a document create a range where start = end.

• newText : String

  The string to be inserted. For delete operations use an empty string.

• leanExtSnippet? : Option Lean.Lsp.SnippetString

  If this field is present and the editor supports it, newText is ignored and an interactive snippet edit is performed instead.

  The use of snippets in TextEdits is a Lean-specific extension to the LSP standard, so newText should still be set to a correct value as fallback in case the editor does not support this feature. Even editors that support snippets may not always use them; for instance, if the file is not already open, VS Code will perform a normal text edit in the background instead.

• annotationId? : Option String

  Identifier for annotated edit.

  WorkspaceEdit has a changeAnnotations field that maps these identifiers to a ChangeAnnotation. By annotating an edit you can add a description of what the edit will do and also control whether the user is presented with a prompt before applying the edit. reference.

instance Lean.Lsp.instToJsonTextEdit : Lean.ToJson Lean.Lsp.TextEdit

Equations

• Lean.Lsp.instToJsonTextEdit = { toJson := Lean.Lsp.toJsonTextEdit✝ }

instance Lean.Lsp.instFromJsonTextEdit : Lean.FromJson Lean.Lsp.TextEdit

Equations

• Lean.Lsp.instFromJsonTextEdit = { fromJson? := Lean.Lsp.fromJsonTextEdit✝ }

def Lean.Lsp.TextEditBatch : Type

An array of TextEdits to be performed in sequence.

Equations

• Lean.Lsp.TextEditBatch = Array Lean.Lsp.TextEdit

instance Lean.Lsp.instFromJsonTextEditBatch : Lean.FromJson Lean.Lsp.TextEditBatch

Equations

• Lean.Lsp.instFromJsonTextEditBatch = { fromJson? := Lean.fromJson? }

instance Lean.Lsp.instToJsonTextEditBatch : Lean.ToJson Lean.Lsp.TextEditBatch

Equations

• Lean.Lsp.instToJsonTextEditBatch = { toJson := Lean.toJson }

instance Lean.Lsp.instEmptyCollectionTextEditBatch : EmptyCollection Lean.Lsp.TextEditBatch

Equations

• Lean.Lsp.instEmptyCollectionTextEditBatch = { emptyCollection := #[] }

instance Lean.Lsp.instAppendTextEditBatch : Append Lean.Lsp.TextEditBatch

Equations

• Lean.Lsp.instAppendTextEditBatch = inferInstanceAs (Append (Array Lean.Lsp.TextEdit))

instance Lean.Lsp.instCoeTextEditTextEditBatch : Coe Lean.Lsp.TextEdit Lean.Lsp.TextEditBatch

Equations

• Lean.Lsp.instCoeTextEditTextEditBatch = { coe := fun (te : Lean.Lsp.TextEdit) => #[te] }

structure Lean.Lsp.TextDocumentIdentifier : Type

• uri : Lean.Lsp.DocumentUri

instance Lean.Lsp.instToJsonTextDocumentIdentifier : Lean.ToJson Lean.Lsp.TextDocumentIdentifier

Equations

• Lean.Lsp.instToJsonTextDocumentIdentifier = { toJson := Lean.Lsp.toJsonTextDocumentIdentifier✝ }

instance Lean.Lsp.instFromJsonTextDocumentIdentifier : Lean.FromJson Lean.Lsp.TextDocumentIdentifier

Equations

• Lean.Lsp.instFromJsonTextDocumentIdentifier = { fromJson? := Lean.Lsp.fromJsonTextDocumentIdentifier✝ }

structure Lean.Lsp.VersionedTextDocumentIdentifier : Type

• uri : Lean.Lsp.DocumentUri
• version? : Option Nat

instance Lean.Lsp.instToJsonVersionedTextDocumentIdentifier : Lean.ToJson Lean.Lsp.VersionedTextDocumentIdentifier

Equations

• Lean.Lsp.instToJsonVersionedTextDocumentIdentifier = { toJson := Lean.Lsp.toJsonVersionedTextDocumentIdentifier✝ }

instance Lean.Lsp.instFromJsonVersionedTextDocumentIdentifier : Lean.FromJson Lean.Lsp.VersionedTextDocumentIdentifier

Equations

• Lean.Lsp.instFromJsonVersionedTextDocumentIdentifier = { fromJson? := Lean.Lsp.fromJsonVersionedTextDocumentIdentifier✝ }

structure Lean.Lsp.TextDocumentEdit : Type

A batch of TextEdits to perform on a versioned text document.

reference

• textDocument : Lean.Lsp.VersionedTextDocumentIdentifier
• edits : Lean.Lsp.TextEditBatch

instance Lean.Lsp.instToJsonTextDocumentEdit : Lean.ToJson Lean.Lsp.TextDocumentEdit

Equations

• Lean.Lsp.instToJsonTextDocumentEdit = { toJson := Lean.Lsp.toJsonTextDocumentEdit✝ }

instance Lean.Lsp.instFromJsonTextDocumentEdit : Lean.FromJson Lean.Lsp.TextDocumentEdit

Equations

• Lean.Lsp.instFromJsonTextDocumentEdit = { fromJson? := Lean.Lsp.fromJsonTextDocumentEdit✝ }

structure Lean.Lsp.ChangeAnnotation : Type

Additional information that describes document changes.

reference

• label : String

  A human-readable string describing the actual change. The string is rendered prominent in the user interface.

• needsConfirmation : Bool

  A flag which indicates that user confirmation is needed before applying the change.

• description? : Option String

  A human-readable string which is rendered less prominent in the user interface.

instance Lean.Lsp.instToJsonChangeAnnotation : Lean.ToJson Lean.Lsp.ChangeAnnotation

Equations

• Lean.Lsp.instToJsonChangeAnnotation = { toJson := Lean.Lsp.toJsonChangeAnnotation✝ }

instance Lean.Lsp.instFromJsonChangeAnnotation : Lean.FromJson Lean.Lsp.ChangeAnnotation

Equations

• Lean.Lsp.instFromJsonChangeAnnotation = { fromJson? := Lean.Lsp.fromJsonChangeAnnotation✝ }

structure Lean.Lsp.CreateFile.Options : Type

Options for CreateFile and RenameFile.

• overwrite : Bool
• ignoreIfExists : Bool

instance Lean.Lsp.CreateFile.instToJsonOptions : Lean.ToJson Lean.Lsp.CreateFile.Options

Equations

• Lean.Lsp.CreateFile.instToJsonOptions = { toJson := Lean.Lsp.CreateFile.toJsonOptions✝ }

instance Lean.Lsp.CreateFile.instFromJsonOptions : Lean.FromJson Lean.Lsp.CreateFile.Options

Equations

• Lean.Lsp.CreateFile.instFromJsonOptions = { fromJson? := Lean.Lsp.CreateFile.fromJsonOptions✝ }

structure Lean.Lsp.DeleteFile.Options : Type

Options for DeleteFile.

• recursive : Bool
• ignoreIfNotExists : Bool

instance Lean.Lsp.DeleteFile.instToJsonOptions : Lean.ToJson Lean.Lsp.DeleteFile.Options

Equations

• Lean.Lsp.DeleteFile.instToJsonOptions = { toJson := Lean.Lsp.DeleteFile.toJsonOptions✝ }

instance Lean.Lsp.DeleteFile.instFromJsonOptions : Lean.FromJson Lean.Lsp.DeleteFile.Options

Equations

• Lean.Lsp.DeleteFile.instFromJsonOptions = { fromJson? := Lean.Lsp.DeleteFile.fromJsonOptions✝ }

structure Lean.Lsp.CreateFile : Type

• uri : Lean.Lsp.DocumentUri
• options? : Option Lean.Lsp.CreateFile.Options
• annotationId? : Option String

instance Lean.Lsp.instToJsonCreateFile : Lean.ToJson Lean.Lsp.CreateFile

Equations

• Lean.Lsp.instToJsonCreateFile = { toJson := Lean.Lsp.toJsonCreateFile✝ }

instance Lean.Lsp.instFromJsonCreateFile : Lean.FromJson Lean.Lsp.CreateFile

Equations

• Lean.Lsp.instFromJsonCreateFile = { fromJson? := Lean.Lsp.fromJsonCreateFile✝ }

structure Lean.Lsp.RenameFile : Type

• oldUri : Lean.Lsp.DocumentUri
• newUri : Lean.Lsp.DocumentUri
• options? : Option Lean.Lsp.CreateFile.Options
• annotationId? : Option String

instance Lean.Lsp.instToJsonRenameFile : Lean.ToJson Lean.Lsp.RenameFile

Equations

• Lean.Lsp.instToJsonRenameFile = { toJson := Lean.Lsp.toJsonRenameFile✝ }

instance Lean.Lsp.instFromJsonRenameFile : Lean.FromJson Lean.Lsp.RenameFile

Equations

• Lean.Lsp.instFromJsonRenameFile = { fromJson? := Lean.Lsp.fromJsonRenameFile✝ }

structure Lean.Lsp.DeleteFile : Type

• uri : Lean.Lsp.DocumentUri
• options? : Option Lean.Lsp.DeleteFile.Options
• annotationId? : Option String

instance Lean.Lsp.instToJsonDeleteFile : Lean.ToJson Lean.Lsp.DeleteFile

Equations

• Lean.Lsp.instToJsonDeleteFile = { toJson := Lean.Lsp.toJsonDeleteFile✝ }

instance Lean.Lsp.instFromJsonDeleteFile : Lean.FromJson Lean.Lsp.DeleteFile

Equations

• Lean.Lsp.instFromJsonDeleteFile = { fromJson? := Lean.Lsp.fromJsonDeleteFile✝ }

inductive Lean.Lsp.DocumentChange : Type

A change to a file resource.

reference

• create: Lean.Lsp.CreateFile → Lean.Lsp.DocumentChange
• rename: Lean.Lsp.RenameFile → Lean.Lsp.DocumentChange
• delete: Lean.Lsp.DeleteFile → Lean.Lsp.DocumentChange
• edit: Lean.Lsp.TextDocumentEdit → Lean.Lsp.DocumentChange

instance Lean.Lsp.instToJsonDocumentChange : Lean.ToJson Lean.Lsp.DocumentChange

Equations

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

instance Lean.Lsp.instFromJsonDocumentChange : Lean.FromJson Lean.Lsp.DocumentChange

Equations

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

structure Lean.Lsp.WorkspaceEdit : Type

A workspace edit represents changes to many resources managed in the workspace.

reference

• changes? : Option (Lean.RBMap Lean.Lsp.DocumentUri Lean.Lsp.TextEditBatch compare)

  Changes to existing resources.

• documentChanges? : Option (Array Lean.Lsp.DocumentChange)

  Depending on the client capability workspace.workspaceEdit.resourceOperations document changes are either an array of TextDocumentEdits to express changes to n different text documents where each text document edit addresses a specific version of a text document. Or it can contain above TextDocumentEdits mixed with create, rename and delete file / folder operations.

  Whether a client supports versioned document edits is expressed via workspace.workspaceEdit.documentChanges client capability.

  If a client neither supports documentChanges nor workspace.workspaceEdit.resourceOperations then only plain TextEdits using the changes property are supported.

• changeAnnotations? : Option (Lean.RBMap String Lean.Lsp.ChangeAnnotation compare)

  A map of change annotations that can be referenced in AnnotatedTextEdits or create, rename and delete file / folder operations.

  Whether clients honor this property depends on the client capability workspace.changeAnnotationSupport.

instance Lean.Lsp.instToJsonWorkspaceEdit : Lean.ToJson Lean.Lsp.WorkspaceEdit

Equations

• Lean.Lsp.instToJsonWorkspaceEdit = { toJson := Lean.Lsp.toJsonWorkspaceEdit✝ }

instance Lean.Lsp.instFromJsonWorkspaceEdit : Lean.FromJson Lean.Lsp.WorkspaceEdit

Equations

• Lean.Lsp.instFromJsonWorkspaceEdit = { fromJson? := Lean.Lsp.fromJsonWorkspaceEdit✝ }

instance Lean.Lsp.WorkspaceEdit.instEmptyCollectionWorkspaceEdit : EmptyCollection Lean.Lsp.WorkspaceEdit

Equations

• Lean.Lsp.WorkspaceEdit.instEmptyCollectionWorkspaceEdit = { emptyCollection := { changes? := none, documentChanges? := none, changeAnnotations? := none } }

instance Lean.Lsp.WorkspaceEdit.instAppendWorkspaceEdit : Append Lean.Lsp.WorkspaceEdit

Equations

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

def Lean.Lsp.WorkspaceEdit.ofTextDocumentEdit (e : Lean.Lsp.TextDocumentEdit) : Lean.Lsp.WorkspaceEdit

Equations

• Lean.Lsp.WorkspaceEdit.ofTextDocumentEdit e = { changes? := none, documentChanges? := some #[Lean.Lsp.DocumentChange.edit e], changeAnnotations? := none }

def Lean.Lsp.WorkspaceEdit.ofTextEdit (doc : Lean.Lsp.VersionedTextDocumentIdentifier) (te : Lean.Lsp.TextEdit) : Lean.Lsp.WorkspaceEdit

Equations

• Lean.Lsp.WorkspaceEdit.ofTextEdit doc te = Lean.Lsp.WorkspaceEdit.ofTextDocumentEdit { textDocument := doc, edits := #[te] }

structure Lean.Lsp.ApplyWorkspaceEditParams : Type

The workspace/applyEdit request is sent from the server to the client to modify resource on the client side.

reference

• label? : Option String

  An optional label of the workspace edit. This label is presented in the user interface for example on an undo stack to undo the workspace edit.

• edit : Lean.Lsp.WorkspaceEdit

  The edits to apply.

instance Lean.Lsp.instToJsonApplyWorkspaceEditParams : Lean.ToJson Lean.Lsp.ApplyWorkspaceEditParams

Equations

• Lean.Lsp.instToJsonApplyWorkspaceEditParams = { toJson := Lean.Lsp.toJsonApplyWorkspaceEditParams✝ }

instance Lean.Lsp.instFromJsonApplyWorkspaceEditParams : Lean.FromJson Lean.Lsp.ApplyWorkspaceEditParams

Equations

• Lean.Lsp.instFromJsonApplyWorkspaceEditParams = { fromJson? := Lean.Lsp.fromJsonApplyWorkspaceEditParams✝ }

structure Lean.Lsp.TextDocumentItem : Type

An item to transfer a text document from the client to the server.

reference

• uri : Lean.Lsp.DocumentUri

  The text document's URI.

• languageId : String

  The text document's language identifier.

• version : Nat

  The version number of this document (it will increase after each change, including undo/redo).

• text : String

  The content of the opened text document.

instance Lean.Lsp.instToJsonTextDocumentItem : Lean.ToJson Lean.Lsp.TextDocumentItem

Equations

• Lean.Lsp.instToJsonTextDocumentItem = { toJson := Lean.Lsp.toJsonTextDocumentItem✝ }

instance Lean.Lsp.instFromJsonTextDocumentItem : Lean.FromJson Lean.Lsp.TextDocumentItem

Equations

• Lean.Lsp.instFromJsonTextDocumentItem = { fromJson? := Lean.Lsp.fromJsonTextDocumentItem✝ }

structure Lean.Lsp.TextDocumentPositionParams : Type

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

instance Lean.Lsp.instToJsonTextDocumentPositionParams : Lean.ToJson Lean.Lsp.TextDocumentPositionParams

Equations

• Lean.Lsp.instToJsonTextDocumentPositionParams = { toJson := Lean.Lsp.toJsonTextDocumentPositionParams✝ }

instance Lean.Lsp.instFromJsonTextDocumentPositionParams : Lean.FromJson Lean.Lsp.TextDocumentPositionParams

Equations

• Lean.Lsp.instFromJsonTextDocumentPositionParams = { fromJson? := Lean.Lsp.fromJsonTextDocumentPositionParams✝ }

instance Lean.Lsp.instToStringTextDocumentPositionParams : ToString Lean.Lsp.TextDocumentPositionParams

Equations

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

structure Lean.Lsp.DocumentFilter : Type

• language? : Option String
• scheme? : Option String
• pattern? : Option String

instance Lean.Lsp.instToJsonDocumentFilter : Lean.ToJson Lean.Lsp.DocumentFilter

Equations

• Lean.Lsp.instToJsonDocumentFilter = { toJson := Lean.Lsp.toJsonDocumentFilter✝ }

instance Lean.Lsp.instFromJsonDocumentFilter : Lean.FromJson Lean.Lsp.DocumentFilter

Equations

• Lean.Lsp.instFromJsonDocumentFilter = { fromJson? := Lean.Lsp.fromJsonDocumentFilter✝ }

def Lean.Lsp.DocumentSelector : Type

Equations

• Lean.Lsp.DocumentSelector = Array Lean.Lsp.DocumentFilter

instance Lean.Lsp.instFromJsonDocumentSelector : Lean.FromJson Lean.Lsp.DocumentSelector

Equations

• Lean.Lsp.instFromJsonDocumentSelector = { fromJson? := Lean.fromJson? }

instance Lean.Lsp.instToJsonDocumentSelector : Lean.ToJson Lean.Lsp.DocumentSelector

Equations

• Lean.Lsp.instToJsonDocumentSelector = { toJson := Lean.toJson }

structure Lean.Lsp.StaticRegistrationOptions : Type

• id? : Option String

instance Lean.Lsp.instToJsonStaticRegistrationOptions : Lean.ToJson Lean.Lsp.StaticRegistrationOptions

Equations

• Lean.Lsp.instToJsonStaticRegistrationOptions = { toJson := Lean.Lsp.toJsonStaticRegistrationOptions✝ }

instance Lean.Lsp.instFromJsonStaticRegistrationOptions : Lean.FromJson Lean.Lsp.StaticRegistrationOptions

Equations

• Lean.Lsp.instFromJsonStaticRegistrationOptions = { fromJson? := Lean.Lsp.fromJsonStaticRegistrationOptions✝ }

structure Lean.Lsp.TextDocumentRegistrationOptions : Type

• documentSelector? : Option Lean.Lsp.DocumentSelector

instance Lean.Lsp.instToJsonTextDocumentRegistrationOptions : Lean.ToJson Lean.Lsp.TextDocumentRegistrationOptions

Equations

• Lean.Lsp.instToJsonTextDocumentRegistrationOptions = { toJson := Lean.Lsp.toJsonTextDocumentRegistrationOptions✝ }

instance Lean.Lsp.instFromJsonTextDocumentRegistrationOptions : Lean.FromJson Lean.Lsp.TextDocumentRegistrationOptions

Equations

• Lean.Lsp.instFromJsonTextDocumentRegistrationOptions = { fromJson? := Lean.Lsp.fromJsonTextDocumentRegistrationOptions✝ }

inductive Lean.Lsp.MarkupKind : Type

• plaintext: Lean.Lsp.MarkupKind
• markdown: Lean.Lsp.MarkupKind

instance Lean.Lsp.instFromJsonMarkupKind : Lean.FromJson Lean.Lsp.MarkupKind

Equations

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

instance Lean.Lsp.instToJsonMarkupKind : Lean.ToJson Lean.Lsp.MarkupKind

Equations

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

structure Lean.Lsp.MarkupContent : Type

• kind : Lean.Lsp.MarkupKind
• value : String

instance Lean.Lsp.instToJsonMarkupContent : Lean.ToJson Lean.Lsp.MarkupContent

Equations

• Lean.Lsp.instToJsonMarkupContent = { toJson := Lean.Lsp.toJsonMarkupContent✝ }

instance Lean.Lsp.instFromJsonMarkupContent : Lean.FromJson Lean.Lsp.MarkupContent

Equations

• Lean.Lsp.instFromJsonMarkupContent = { fromJson? := Lean.Lsp.fromJsonMarkupContent✝ }

@[inline, reducible]

abbrev Lean.Lsp.ProgressToken : Type

Reference to the progress of some in-flight piece of work.

reference

Equations

• Lean.Lsp.ProgressToken = String

structure Lean.Lsp.ProgressParams (α : Type) : Type

Params for JSON-RPC method $/progress request.

reference

• token : Lean.Lsp.ProgressToken
• value : α

instance Lean.Lsp.instToJsonProgressParams : {α : Type} → [inst : Lean.ToJson α] → Lean.ToJson (Lean.Lsp.ProgressParams α)

Equations

• Lean.Lsp.instToJsonProgressParams = { toJson := Lean.Lsp.toJsonProgressParams✝ }

structure Lean.Lsp.WorkDoneProgressReport : Type

• kind : String
• message? : Option String

  More detailed associated progress message.

• cancellable : Bool

  Controls if a cancel button should show to allow the user to cancel the operation.

• percentage? : Option Nat

  Optional progress percentage to display (value 100 is considered 100%). If not provided infinite progress is assumed.

instance Lean.Lsp.instToJsonWorkDoneProgressReport : Lean.ToJson Lean.Lsp.WorkDoneProgressReport

Equations

• Lean.Lsp.instToJsonWorkDoneProgressReport = { toJson := Lean.Lsp.toJsonWorkDoneProgressReport✝ }

structure Lean.Lsp.WorkDoneProgressBeginextends Lean.Lsp.WorkDoneProgressReport : Type

Notification to signal the start of progress reporting.

• kind : String
• message? : Option String
• cancellable : Bool
• percentage? : Option Nat
• title : String

instance Lean.Lsp.instToJsonWorkDoneProgressBegin : Lean.ToJson Lean.Lsp.WorkDoneProgressBegin

Equations

• Lean.Lsp.instToJsonWorkDoneProgressBegin = { toJson := Lean.Lsp.toJsonWorkDoneProgressBegin✝ }

structure Lean.Lsp.WorkDoneProgressEnd : Type

Signals the end of progress reporting.

• kind : String
• message? : Option String

instance Lean.Lsp.instToJsonWorkDoneProgressEnd : Lean.ToJson Lean.Lsp.WorkDoneProgressEnd

Equations

• Lean.Lsp.instToJsonWorkDoneProgressEnd = { toJson := Lean.Lsp.toJsonWorkDoneProgressEnd✝ }

structure Lean.Lsp.WorkDoneProgressParams : Type

• workDoneToken? : Option Lean.Lsp.ProgressToken

instance Lean.Lsp.instToJsonWorkDoneProgressParams : Lean.ToJson Lean.Lsp.WorkDoneProgressParams

Equations

• Lean.Lsp.instToJsonWorkDoneProgressParams = { toJson := Lean.Lsp.toJsonWorkDoneProgressParams✝ }

instance Lean.Lsp.instFromJsonWorkDoneProgressParams : Lean.FromJson Lean.Lsp.WorkDoneProgressParams

Equations

• Lean.Lsp.instFromJsonWorkDoneProgressParams = { fromJson? := Lean.Lsp.fromJsonWorkDoneProgressParams✝ }

structure Lean.Lsp.PartialResultParams : Type

• partialResultToken? : Option Lean.Lsp.ProgressToken

instance Lean.Lsp.instToJsonPartialResultParams : Lean.ToJson Lean.Lsp.PartialResultParams

Equations

• Lean.Lsp.instToJsonPartialResultParams = { toJson := Lean.Lsp.toJsonPartialResultParams✝ }

instance Lean.Lsp.instFromJsonPartialResultParams : Lean.FromJson Lean.Lsp.PartialResultParams

Equations

• Lean.Lsp.instFromJsonPartialResultParams = { fromJson? := Lean.Lsp.fromJsonPartialResultParams✝ }

structure Lean.Lsp.WorkDoneProgressOptions : Type

reference

• workDoneProgress : Bool

instance Lean.Lsp.instToJsonWorkDoneProgressOptions : Lean.ToJson Lean.Lsp.WorkDoneProgressOptions

Equations

• Lean.Lsp.instToJsonWorkDoneProgressOptions = { toJson := Lean.Lsp.toJsonWorkDoneProgressOptions✝ }

instance Lean.Lsp.instFromJsonWorkDoneProgressOptions : Lean.FromJson Lean.Lsp.WorkDoneProgressOptions

Equations

• Lean.Lsp.instFromJsonWorkDoneProgressOptions = { fromJson? := Lean.Lsp.fromJsonWorkDoneProgressOptions✝ }