Documentation

Lean.Data.Lsp.InitShutdown

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

Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    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.

        Lean-specific initialization options.

        • 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.

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