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