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

A Location is a DocumentUri and a Range.

• uri : DocumentUri
• range : Range

def Lean.Lsp.instInhabitedLocation.default : Location

Equations

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

instance Lean.Lsp.instInhabitedLocation : Inhabited Location

Equations

• Lean.Lsp.instInhabitedLocation = { default := Lean.Lsp.instInhabitedLocation.default }

def Lean.Lsp.instBEqLocation.beq : Location → Location → Bool

Equations

• Lean.Lsp.instBEqLocation.beq { uri := a, range := a_1 } { uri := b, range := b_1 } = (a == b && a_1 == b_1)
• Lean.Lsp.instBEqLocation.beq x✝¹ x✝ = false

instance Lean.Lsp.instBEqLocation : BEq Location

Equations

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

instance Lean.Lsp.instToJsonLocation : ToJson Location

Equations

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

def Lean.Lsp.instToJsonLocation.toJson : Location → Json

Equations

• Lean.Lsp.instToJsonLocation.toJson x✝ = Lean.Json.mkObj [[("uri", Lean.toJson x✝.uri)], [("range", Lean.toJson x✝.range)]].flatten

def Lean.Lsp.instFromJsonLocation.fromJson : Json → Except String Location

Equations

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

instance Lean.Lsp.instFromJsonLocation : FromJson Location

Equations

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

def Lean.Lsp.instOrdLocation.ord : Location → Location → Ordering

Equations

• Lean.Lsp.instOrdLocation.ord { uri := a, range := a_1 } { uri := b, range := b_1 } = (compare a b).then ((compare a_1 b_1).then Ordering.eq)

instance Lean.Lsp.instOrdLocation : Ord Location

Equations

• Lean.Lsp.instOrdLocation = { compare := Lean.Lsp.instOrdLocation.ord }

structure Lean.Lsp.LocationLink : Type

• originSelectionRange? : Option Range
• targetUri : DocumentUri
• targetRange : Range
• targetSelectionRange : Range

def Lean.Lsp.instToJsonLocationLink.toJson : LocationLink → Json

Equations

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

instance Lean.Lsp.instToJsonLocationLink : ToJson LocationLink

Equations

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

def Lean.Lsp.instFromJsonLocationLink.fromJson : Json → Except String LocationLink

Equations

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

instance Lean.Lsp.instFromJsonLocationLink : FromJson LocationLink

Equations

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

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 Json)

  Arguments that the command handler should be invoked with.

def Lean.Lsp.instToJsonCommand.toJson : Command → Json

Equations

• Lean.Lsp.instToJsonCommand.toJson x✝ = Lean.Json.mkObj [[("title", Lean.toJson x✝.title)], [("command", Lean.toJson x✝.command)], Lean.Json.opt "arguments" x✝.arguments?].flatten

instance Lean.Lsp.instToJsonCommand : ToJson Command

Equations

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

instance Lean.Lsp.instFromJsonCommand : FromJson Command

Equations

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

def Lean.Lsp.instFromJsonCommand.fromJson : Json → Except String Command

Equations

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

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

def Lean.Lsp.instToJsonSnippetString.toJson : SnippetString → Json

Equations

• Lean.Lsp.instToJsonSnippetString.toJson x✝ = Lean.Json.mkObj [[("value", Lean.toJson x✝.value)]].flatten

instance Lean.Lsp.instToJsonSnippetString : ToJson SnippetString

Equations

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

instance Lean.Lsp.instFromJsonSnippetString : FromJson SnippetString

Equations

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

def Lean.Lsp.instFromJsonSnippetString.fromJson : Json → Except String SnippetString

Equations

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

structure Lean.Lsp.TextEdit : Type

A textual edit applicable to a text document.

reference

• range : 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 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 : ToJson TextEdit

Equations

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

def Lean.Lsp.instToJsonTextEdit.toJson : TextEdit → Json

Equations

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

instance Lean.Lsp.instFromJsonTextEdit : FromJson TextEdit

Equations

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

def Lean.Lsp.instFromJsonTextEdit.fromJson : Json → Except String TextEdit

Equations

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

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 : FromJson TextEditBatch

Equations

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

instance Lean.Lsp.instToJsonTextEditBatch : ToJson TextEditBatch

Equations

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

instance Lean.Lsp.instEmptyCollectionTextEditBatch : EmptyCollection TextEditBatch

Equations

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

instance Lean.Lsp.instAppendTextEditBatch : Append TextEditBatch

Equations

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

instance Lean.Lsp.instCoeTextEditTextEditBatch : Coe TextEdit TextEditBatch

Equations

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

structure Lean.Lsp.TextDocumentIdentifier : Type

• uri : DocumentUri

def Lean.Lsp.instToJsonTextDocumentIdentifier.toJson : TextDocumentIdentifier → Json

Equations

• Lean.Lsp.instToJsonTextDocumentIdentifier.toJson x✝ = Lean.Json.mkObj [[("uri", Lean.toJson x✝.uri)]].flatten

instance Lean.Lsp.instToJsonTextDocumentIdentifier : ToJson TextDocumentIdentifier

Equations

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

instance Lean.Lsp.instFromJsonTextDocumentIdentifier : FromJson TextDocumentIdentifier

Equations

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

def Lean.Lsp.instFromJsonTextDocumentIdentifier.fromJson : Json → Except String TextDocumentIdentifier

Equations

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

structure Lean.Lsp.VersionedTextDocumentIdentifier : Type

• uri : DocumentUri
• version? : Option Nat

def Lean.Lsp.instToJsonVersionedTextDocumentIdentifier.toJson : VersionedTextDocumentIdentifier → Json

Equations

• Lean.Lsp.instToJsonVersionedTextDocumentIdentifier.toJson x✝ = Lean.Json.mkObj [[("uri", Lean.toJson x✝.uri)], Lean.Json.opt "version" x✝.version?].flatten

instance Lean.Lsp.instToJsonVersionedTextDocumentIdentifier : ToJson VersionedTextDocumentIdentifier

Equations

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

def Lean.Lsp.instFromJsonVersionedTextDocumentIdentifier.fromJson : Json → Except String VersionedTextDocumentIdentifier

Equations

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

instance Lean.Lsp.instFromJsonVersionedTextDocumentIdentifier : FromJson VersionedTextDocumentIdentifier

Equations

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

structure Lean.Lsp.TextDocumentEdit : Type

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

reference

• textDocument : VersionedTextDocumentIdentifier
• edits : TextEditBatch

def Lean.Lsp.instToJsonTextDocumentEdit.toJson : TextDocumentEdit → Json

Equations

• Lean.Lsp.instToJsonTextDocumentEdit.toJson x✝ = Lean.Json.mkObj [[("textDocument", Lean.toJson x✝.textDocument)], [("edits", Lean.toJson x✝.edits)]].flatten

instance Lean.Lsp.instToJsonTextDocumentEdit : ToJson TextDocumentEdit

Equations

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

def Lean.Lsp.instFromJsonTextDocumentEdit.fromJson : Json → Except String TextDocumentEdit

Equations

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

instance Lean.Lsp.instFromJsonTextDocumentEdit : FromJson TextDocumentEdit

Equations

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

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.

def Lean.Lsp.instToJsonChangeAnnotation.toJson : ChangeAnnotation → Json

Equations

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

instance Lean.Lsp.instToJsonChangeAnnotation : ToJson ChangeAnnotation

Equations

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

def Lean.Lsp.instFromJsonChangeAnnotation.fromJson : Json → Except String ChangeAnnotation

Equations

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

instance Lean.Lsp.instFromJsonChangeAnnotation : FromJson ChangeAnnotation

Equations

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

structure Lean.Lsp.CreateFile.Options : Type

Options for CreateFile and RenameFile.

• overwrite : Bool
• ignoreIfExists : Bool

def Lean.Lsp.CreateFile.instToJsonOptions.toJson : Options → Json

Equations

• Lean.Lsp.CreateFile.instToJsonOptions.toJson x✝ = Lean.Json.mkObj [[("overwrite", Lean.toJson x✝.overwrite)], [("ignoreIfExists", Lean.toJson x✝.ignoreIfExists)]].flatten

instance Lean.Lsp.CreateFile.instToJsonOptions : ToJson Options

Equations

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

instance Lean.Lsp.CreateFile.instFromJsonOptions : FromJson Options

Equations

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

def Lean.Lsp.CreateFile.instFromJsonOptions.fromJson : Json → Except String Options

Equations

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

structure Lean.Lsp.DeleteFile.Options : Type

Options for DeleteFile.

• recursive : Bool
• ignoreIfNotExists : Bool

instance Lean.Lsp.DeleteFile.instToJsonOptions : ToJson Options

Equations

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

def Lean.Lsp.DeleteFile.instToJsonOptions.toJson : Options → Json

Equations

• Lean.Lsp.DeleteFile.instToJsonOptions.toJson x✝ = Lean.Json.mkObj [[("recursive", Lean.toJson x✝.recursive)], [("ignoreIfNotExists", Lean.toJson x✝.ignoreIfNotExists)]].flatten

instance Lean.Lsp.DeleteFile.instFromJsonOptions : FromJson Options

Equations

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

def Lean.Lsp.DeleteFile.instFromJsonOptions.fromJson : Json → Except String Options

Equations

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

structure Lean.Lsp.CreateFile : Type

• uri : DocumentUri
• options? : Option Options
• annotationId? : Option String

def Lean.Lsp.instToJsonCreateFile.toJson : CreateFile → Json

Equations

• Lean.Lsp.instToJsonCreateFile.toJson x✝ = Lean.Json.mkObj [[("uri", Lean.toJson x✝.uri)], Lean.Json.opt "options" x✝.options?, Lean.Json.opt "annotationId" x✝.annotationId?].flatten

instance Lean.Lsp.instToJsonCreateFile : ToJson CreateFile

Equations

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

def Lean.Lsp.instFromJsonCreateFile.fromJson : Json → Except String CreateFile

Equations

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

instance Lean.Lsp.instFromJsonCreateFile : FromJson CreateFile

Equations

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

structure Lean.Lsp.RenameFile : Type

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

instance Lean.Lsp.instToJsonRenameFile : ToJson RenameFile

Equations

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

def Lean.Lsp.instToJsonRenameFile.toJson : RenameFile → Json

Equations

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

instance Lean.Lsp.instFromJsonRenameFile : FromJson RenameFile

Equations

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

def Lean.Lsp.instFromJsonRenameFile.fromJson : Json → Except String RenameFile

Equations

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

structure Lean.Lsp.DeleteFile : Type

• uri : DocumentUri
• options? : Option Options
• annotationId? : Option String

instance Lean.Lsp.instToJsonDeleteFile : ToJson DeleteFile

Equations

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

def Lean.Lsp.instToJsonDeleteFile.toJson : DeleteFile → Json

Equations

• Lean.Lsp.instToJsonDeleteFile.toJson x✝ = Lean.Json.mkObj [[("uri", Lean.toJson x✝.uri)], Lean.Json.opt "options" x✝.options?, Lean.Json.opt "annotationId" x✝.annotationId?].flatten

instance Lean.Lsp.instFromJsonDeleteFile : FromJson DeleteFile

Equations

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

def Lean.Lsp.instFromJsonDeleteFile.fromJson : Json → Except String DeleteFile

Equations

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

inductive Lean.Lsp.DocumentChange : Type

A change to a file resource.

reference

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

instance Lean.Lsp.instToJsonDocumentChange : ToJson DocumentChange

Equations

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

instance Lean.Lsp.instFromJsonDocumentChange : FromJson 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 (Std.TreeMap DocumentUri TextEditBatch compare)

  Changes to existing resources.

• documentChanges? : Option (Array 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 (Std.TreeMap String 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 : ToJson WorkspaceEdit

Equations

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

def Lean.Lsp.instToJsonWorkspaceEdit.toJson : WorkspaceEdit → Json

Equations

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

instance Lean.Lsp.instFromJsonWorkspaceEdit : FromJson WorkspaceEdit

Equations

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

def Lean.Lsp.instFromJsonWorkspaceEdit.fromJson : Json → Except String WorkspaceEdit

Equations

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

instance Lean.Lsp.WorkspaceEdit.instEmptyCollection : EmptyCollection WorkspaceEdit

Equations

• Lean.Lsp.WorkspaceEdit.instEmptyCollection = { emptyCollection := { } }

instance Lean.Lsp.WorkspaceEdit.instAppend : Append WorkspaceEdit

Equations

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

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

Equations

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

def Lean.Lsp.WorkspaceEdit.ofTextEdit (doc : VersionedTextDocumentIdentifier) (te : TextEdit) : 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 : WorkspaceEdit

  The edits to apply.

def Lean.Lsp.instToJsonApplyWorkspaceEditParams.toJson : ApplyWorkspaceEditParams → Json

Equations

• Lean.Lsp.instToJsonApplyWorkspaceEditParams.toJson x✝ = Lean.Json.mkObj [Lean.Json.opt "label" x✝.label?, [("edit", Lean.toJson x✝.edit)]].flatten

instance Lean.Lsp.instToJsonApplyWorkspaceEditParams : ToJson ApplyWorkspaceEditParams

Equations

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

instance Lean.Lsp.instFromJsonApplyWorkspaceEditParams : FromJson ApplyWorkspaceEditParams

Equations

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

def Lean.Lsp.instFromJsonApplyWorkspaceEditParams.fromJson : Json → Except String ApplyWorkspaceEditParams

Equations

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

structure Lean.Lsp.TextDocumentItem : Type

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

reference

• uri : 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 : ToJson TextDocumentItem

Equations

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

def Lean.Lsp.instToJsonTextDocumentItem.toJson : TextDocumentItem → Json

Equations

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

instance Lean.Lsp.instFromJsonTextDocumentItem : FromJson TextDocumentItem

Equations

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

def Lean.Lsp.instFromJsonTextDocumentItem.fromJson : Json → Except String TextDocumentItem

Equations

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

structure Lean.Lsp.TextDocumentPositionParams : Type

• textDocument : TextDocumentIdentifier
• position : Position

instance Lean.Lsp.instToJsonTextDocumentPositionParams : ToJson TextDocumentPositionParams

Equations

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

def Lean.Lsp.instToJsonTextDocumentPositionParams.toJson : TextDocumentPositionParams → Json

Equations

• Lean.Lsp.instToJsonTextDocumentPositionParams.toJson x✝ = Lean.Json.mkObj [[("textDocument", Lean.toJson x✝.textDocument)], [("position", Lean.toJson x✝.position)]].flatten

def Lean.Lsp.instFromJsonTextDocumentPositionParams.fromJson : Json → Except String TextDocumentPositionParams

Equations

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

instance Lean.Lsp.instFromJsonTextDocumentPositionParams : FromJson TextDocumentPositionParams

Equations

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

instance Lean.Lsp.instToStringTextDocumentPositionParams : ToString 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 : ToJson DocumentFilter

Equations

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

def Lean.Lsp.instToJsonDocumentFilter.toJson : DocumentFilter → Json

Equations

• Lean.Lsp.instToJsonDocumentFilter.toJson x✝ = Lean.Json.mkObj [Lean.Json.opt "language" x✝.language?, Lean.Json.opt "scheme" x✝.scheme?, Lean.Json.opt "pattern" x✝.pattern?].flatten

def Lean.Lsp.instFromJsonDocumentFilter.fromJson : Json → Except String DocumentFilter

Equations

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

instance Lean.Lsp.instFromJsonDocumentFilter : FromJson DocumentFilter

Equations

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

def Lean.Lsp.DocumentSelector : Type

Equations

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

instance Lean.Lsp.instFromJsonDocumentSelector : FromJson DocumentSelector

Equations

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

instance Lean.Lsp.instToJsonDocumentSelector : ToJson DocumentSelector

Equations

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

structure Lean.Lsp.StaticRegistrationOptions : Type

• id? : Option String

def Lean.Lsp.instToJsonStaticRegistrationOptions.toJson : StaticRegistrationOptions → Json

Equations

• Lean.Lsp.instToJsonStaticRegistrationOptions.toJson x✝ = Lean.Json.mkObj [Lean.Json.opt "id" x✝.id?].flatten

instance Lean.Lsp.instToJsonStaticRegistrationOptions : ToJson StaticRegistrationOptions

Equations

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

def Lean.Lsp.instFromJsonStaticRegistrationOptions.fromJson : Json → Except String StaticRegistrationOptions

Equations

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

instance Lean.Lsp.instFromJsonStaticRegistrationOptions : FromJson StaticRegistrationOptions

Equations

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

structure Lean.Lsp.TextDocumentRegistrationOptions : Type

• documentSelector? : Option DocumentSelector

def Lean.Lsp.instToJsonTextDocumentRegistrationOptions.toJson : TextDocumentRegistrationOptions → Json

Equations

• Lean.Lsp.instToJsonTextDocumentRegistrationOptions.toJson x✝ = Lean.Json.mkObj [Lean.Json.opt "documentSelector" x✝.documentSelector?].flatten

instance Lean.Lsp.instToJsonTextDocumentRegistrationOptions : ToJson TextDocumentRegistrationOptions

Equations

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

instance Lean.Lsp.instFromJsonTextDocumentRegistrationOptions : FromJson TextDocumentRegistrationOptions

Equations

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

def Lean.Lsp.instFromJsonTextDocumentRegistrationOptions.fromJson : Json → Except String TextDocumentRegistrationOptions

Equations

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

inductive Lean.Lsp.MarkupKind : Type

• plaintext : MarkupKind
• markdown : MarkupKind

instance Lean.Lsp.instDecidableEqMarkupKind : DecidableEq MarkupKind

Equations

• Lean.Lsp.instDecidableEqMarkupKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Lean.Lsp.instHashableMarkupKind.hash : MarkupKind → UInt64

Equations

• Lean.Lsp.instHashableMarkupKind.hash Lean.Lsp.MarkupKind.plaintext = 0
• Lean.Lsp.instHashableMarkupKind.hash Lean.Lsp.MarkupKind.markdown = 1

instance Lean.Lsp.instHashableMarkupKind : Hashable MarkupKind

Equations

• Lean.Lsp.instHashableMarkupKind = { hash := Lean.Lsp.instHashableMarkupKind.hash }

instance Lean.Lsp.instFromJsonMarkupKind : FromJson MarkupKind

Equations

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

instance Lean.Lsp.instToJsonMarkupKind : ToJson MarkupKind

Equations

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

structure Lean.Lsp.MarkupContent : Type

• kind : MarkupKind
• value : String

def Lean.Lsp.instToJsonMarkupContent.toJson : MarkupContent → Json

Equations

• Lean.Lsp.instToJsonMarkupContent.toJson x✝ = Lean.Json.mkObj [[("kind", Lean.toJson x✝.kind)], [("value", Lean.toJson x✝.value)]].flatten

instance Lean.Lsp.instToJsonMarkupContent : ToJson MarkupContent

Equations

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

instance Lean.Lsp.instFromJsonMarkupContent : FromJson MarkupContent

Equations

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

def Lean.Lsp.instFromJsonMarkupContent.fromJson : Json → Except String MarkupContent

Equations

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

def Lean.Lsp.instDecidableEqMarkupContent.decEq (x✝ x✝¹ : MarkupContent) : Decidable (x✝ = x✝¹)

Equations

• Lean.Lsp.instDecidableEqMarkupContent.decEq { kind := a, value := a_1 } { kind := b, value := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance Lean.Lsp.instDecidableEqMarkupContent : DecidableEq MarkupContent

Equations

• Lean.Lsp.instDecidableEqMarkupContent = Lean.Lsp.instDecidableEqMarkupContent.decEq

def Lean.Lsp.instHashableMarkupContent.hash : MarkupContent → UInt64

Equations

• Lean.Lsp.instHashableMarkupContent.hash { kind := a, value := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

instance Lean.Lsp.instHashableMarkupContent : Hashable MarkupContent

Equations

• Lean.Lsp.instHashableMarkupContent = { hash := Lean.Lsp.instHashableMarkupContent.hash }

@[reducible, inline]

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 : ProgressToken
• value : α

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

Equations

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

def Lean.Lsp.instToJsonProgressParams.toJson {α✝ : Type} [ToJson α✝] : ProgressParams α✝ → Json

Equations

• Lean.Lsp.instToJsonProgressParams.toJson x✝ = Lean.Json.mkObj [[("token", Lean.toJson x✝.token)], [("value", Lean.toJson x✝.value)]].flatten

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 : ToJson WorkDoneProgressReport

Equations

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

def Lean.Lsp.instToJsonWorkDoneProgressReport.toJson : WorkDoneProgressReport → Json

Equations

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

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 : ToJson WorkDoneProgressBegin

Equations

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

def Lean.Lsp.instToJsonWorkDoneProgressBegin.toJson : WorkDoneProgressBegin → Json

Equations

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

structure Lean.Lsp.WorkDoneProgressEnd : Type

Signals the end of progress reporting.

• kind : String
• message? : Option String

def Lean.Lsp.instToJsonWorkDoneProgressEnd.toJson : WorkDoneProgressEnd → Json

Equations

• Lean.Lsp.instToJsonWorkDoneProgressEnd.toJson x✝ = Lean.Json.mkObj [[("kind", Lean.toJson x✝.kind)], Lean.Json.opt "message" x✝.message?].flatten

instance Lean.Lsp.instToJsonWorkDoneProgressEnd : ToJson WorkDoneProgressEnd

Equations

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

structure Lean.Lsp.WorkDoneProgressParams : Type

• workDoneToken? : Option ProgressToken

instance Lean.Lsp.instToJsonWorkDoneProgressParams : ToJson WorkDoneProgressParams

Equations

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

def Lean.Lsp.instToJsonWorkDoneProgressParams.toJson : WorkDoneProgressParams → Json

Equations

• Lean.Lsp.instToJsonWorkDoneProgressParams.toJson x✝ = Lean.Json.mkObj [Lean.Json.opt "workDoneToken" x✝.workDoneToken?].flatten

def Lean.Lsp.instFromJsonWorkDoneProgressParams.fromJson : Json → Except String WorkDoneProgressParams

Equations

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

instance Lean.Lsp.instFromJsonWorkDoneProgressParams : FromJson WorkDoneProgressParams

Equations

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

structure Lean.Lsp.PartialResultParams : Type

• partialResultToken? : Option ProgressToken

instance Lean.Lsp.instToJsonPartialResultParams : ToJson PartialResultParams

Equations

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

def Lean.Lsp.instToJsonPartialResultParams.toJson : PartialResultParams → Json

Equations

• Lean.Lsp.instToJsonPartialResultParams.toJson x✝ = Lean.Json.mkObj [Lean.Json.opt "partialResultToken" x✝.partialResultToken?].flatten

instance Lean.Lsp.instFromJsonPartialResultParams : FromJson PartialResultParams

Equations

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

def Lean.Lsp.instFromJsonPartialResultParams.fromJson : Json → Except String PartialResultParams

Equations

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

structure Lean.Lsp.WorkDoneProgressOptions : Type

reference

• workDoneProgress : Bool

def Lean.Lsp.instToJsonWorkDoneProgressOptions.toJson : WorkDoneProgressOptions → Json

Equations

• Lean.Lsp.instToJsonWorkDoneProgressOptions.toJson x✝ = Lean.Json.mkObj [[("workDoneProgress", Lean.toJson x✝.workDoneProgress)]].flatten

instance Lean.Lsp.instToJsonWorkDoneProgressOptions : ToJson WorkDoneProgressOptions

Equations

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

def Lean.Lsp.instFromJsonWorkDoneProgressOptions.fromJson : Json → Except String WorkDoneProgressOptions

Equations

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

instance Lean.Lsp.instFromJsonWorkDoneProgressOptions : FromJson WorkDoneProgressOptions

Equations

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

structure Lean.Lsp.ResolveSupport : Type

• properties : Array String

def Lean.Lsp.instFromJsonResolveSupport.fromJson : Json → Except String ResolveSupport

Equations

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

instance Lean.Lsp.instFromJsonResolveSupport : FromJson ResolveSupport

Equations

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

def Lean.Lsp.instToJsonResolveSupport.toJson : ResolveSupport → Json

Equations

• Lean.Lsp.instToJsonResolveSupport.toJson x✝ = Lean.Json.mkObj [[("properties", Lean.toJson x✝.properties)]].flatten

instance Lean.Lsp.instToJsonResolveSupport : ToJson ResolveSupport

Equations

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