Documentation

Lean.Data.Lsp.Diagnostics

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

LSP: Diagnostic; LSP: textDocument/publishDiagnostics

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.

Some languages have specific codes for each error type.

Instances For
    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.

    Tags representing additional metadata about the diagnostic.

    Instances For
      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

        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
          Equations
          • One or more equations did not get rendered due to their size.
          instance Lean.Lsp.instBEqDiagnosticWith :
          {α : Type} → [inst : BEq α] → BEq (Lean.Lsp.DiagnosticWith α)
          Equations
          • Lean.Lsp.instBEqDiagnosticWith = { beq := Lean.Lsp.beqDiagnosticWith✝ }
          Equations
          • Lean.Lsp.instToJsonDiagnosticWith = { toJson := Lean.Lsp.toJsonDiagnosticWith✝ }
          Equations
          • Lean.Lsp.instFromJsonDiagnosticWith = { fromJson? := Lean.Lsp.fromJsonDiagnosticWith✝ }
          Equations
          • d.fullRange = d.fullRange?.getD d.range
          Instances For
            Equations
            • Lean.Lsp.DiagnosticWith.instOrdUserVisible = { compare := Lean.Lsp.DiagnosticWith.ordUserVisible✝ }
            @[reducible, inline]
            Equations
            Instances For
              Equations