Documentation

Lean.Data.Lsp.InitShutdown

Functionality to do with initializing and shutting down the server ("General Messages" section of LSP spec).

Instances For
    inductive Lean.Lsp.Trace :

    A TraceValue represents the level of verbosity with which the server systematically reports its execution trace using $/logTrace notifications. reference

    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.
      • editDelay? : Option Nat

        Time (in milliseconds) which must pass since latest edit until elaboration begins. Lower values may make editors feel faster at the cost of higher CPU usage. Defaults to 200ms.

      • hasWidgets? : Option Bool

        Whether the client supports interactive widgets. When true, in order to improve performance the server may cease including information which can be retrieved interactively in some standard LSP messages. Defaults to false.

      Lean-specific initialization options.

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