# Documentation

Lean.Data.Lsp.Diagnostics

Definitions and functionality for emitting diagnostic information such as errors, warnings and #command outputs from the LSP server.

Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
• int:
• string:

Some languages have specific codes for each error type.

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

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

Represents a related message and source code location for a diagnostic. This should be used to point to code locations that cause or are related to a diagnostics, e.g when duplicating a symbol in a scope.

Instances For
Equations
• The range at which the message applies.

• Extension: preserve semantic range of errors when truncating them for display purposes.

fullRange? :
• severity? :
• The diagnostic's code, which might appear in the user interface.

code? :
• A human-readable string describing the source of this diagnostic, e.g. 'typescript' or 'super lint'.

source? :
• Parametrised by the type of message data. LSP diagnostics use String, whereas in Lean's interactive diagnostics we use the type of widget-enriched text. See Lean.Widget.InteractiveDiagnostic.

message : α

tags? :
• An array of related diagnostic information, e.g. when symbol-names within a scope collide all definitions can be marked via this property.

relatedInformation? :
• A data entry field that is preserved between a textDocument/publishDiagnostics notification and textDocument/codeAction request.

data? :

Represents a diagnostic, such as a compiler error or warning. Diagnostic objects are only valid in the scope of a resource.

LSP accepts a Diagnostic := DiagnosticWith String. The infoview also accepts InteractiveDiagnostic := DiagnosticWith (TaggedText MsgEmbed).

reference

Instances For
instance Lean.Lsp.instInhabitedDiagnosticWith :
{a : Type} → [inst : ] →
Equations
• One or more equations did not get rendered due to their size.
instance Lean.Lsp.instBEqDiagnosticWith :
{α : Type} → [inst : BEq α] →
Equations
• Lean.Lsp.instBEqDiagnosticWith = { beq := Lean.Lsp.beqDiagnosticWith✝ }
instance Lean.Lsp.instToJsonDiagnosticWith :
{α : Type} → [inst : ] →
Equations
• Lean.Lsp.instToJsonDiagnosticWith = { toJson := Lean.Lsp.toJsonDiagnosticWith✝ }
instance Lean.Lsp.instFromJsonDiagnosticWith :
{α : Type} → [inst : ] →
Equations
• Lean.Lsp.instFromJsonDiagnosticWith = { fromJson? := Lean.Lsp.fromJsonDiagnosticWith✝ }
Equations
@[inline]
Equations
Equations