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

structure Lean.Lsp.ClientInfo : Type

• name : String
• version? : Option String

instance Lean.Lsp.instToJsonClientInfo : Lean.ToJson Lean.Lsp.ClientInfo

Equations

• Lean.Lsp.instToJsonClientInfo = { toJson := Lean.Lsp.toJsonClientInfo✝ }

instance Lean.Lsp.instFromJsonClientInfo : Lean.FromJson Lean.Lsp.ClientInfo

Equations

• Lean.Lsp.instFromJsonClientInfo = { fromJson? := Lean.Lsp.fromJsonClientInfo✝ }

inductive Lean.Lsp.Trace : Type

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

• off : Lean.Lsp.Trace
• messages : Lean.Lsp.Trace
• verbose : Lean.Lsp.Trace

instance Lean.Lsp.instFromJsonTrace : Lean.FromJson Lean.Lsp.Trace

Equations

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

instance Lean.Lsp.Trace.hasToJson : Lean.ToJson Lean.Lsp.Trace

Equations

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

structure Lean.Lsp.InitializationOptions : Type

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.

instance Lean.Lsp.instToJsonInitializationOptions : Lean.ToJson Lean.Lsp.InitializationOptions

Equations

• Lean.Lsp.instToJsonInitializationOptions = { toJson := Lean.Lsp.toJsonInitializationOptions✝ }

instance Lean.Lsp.instFromJsonInitializationOptions : Lean.FromJson Lean.Lsp.InitializationOptions

Equations

• Lean.Lsp.instFromJsonInitializationOptions = { fromJson? := Lean.Lsp.fromJsonInitializationOptions✝ }

structure Lean.Lsp.InitializeParams : Type

• processId? : Option Int
• clientInfo? : Option Lean.Lsp.ClientInfo
• rootUri? : Option String
• initializationOptions? : Option Lean.Lsp.InitializationOptions
• capabilities : Lean.Lsp.ClientCapabilities
• trace : Lean.Lsp.Trace

  If omitted, we default to off.

• workspaceFolders? : Option (Array Lean.Lsp.WorkspaceFolder)

instance Lean.Lsp.instToJsonInitializeParams : Lean.ToJson Lean.Lsp.InitializeParams

Equations

• Lean.Lsp.instToJsonInitializeParams = { toJson := Lean.Lsp.toJsonInitializeParams✝ }

def Lean.Lsp.InitializeParams.editDelay (params : Lean.Lsp.InitializeParams) : Nat

Equations

• params.editDelay = (params.initializationOptions?.bind fun (x : Lean.Lsp.InitializationOptions) => x.editDelay?).getD 200

instance Lean.Lsp.instFromJsonInitializeParams : Lean.FromJson Lean.Lsp.InitializeParams

Equations

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

inductive Lean.Lsp.InitializedParams : Type

• mk : Lean.Lsp.InitializedParams

instance Lean.Lsp.instFromJsonInitializedParams : Lean.FromJson Lean.Lsp.InitializedParams

Equations

• Lean.Lsp.instFromJsonInitializedParams = { fromJson? := fun (x : Lean.Json) => pure Lean.Lsp.InitializedParams.mk }

instance Lean.Lsp.instToJsonInitializedParams : Lean.ToJson Lean.Lsp.InitializedParams

Equations

• Lean.Lsp.instToJsonInitializedParams = { toJson := fun (x : Lean.Lsp.InitializedParams) => Lean.Json.null }

structure Lean.Lsp.ServerInfo : Type

• name : String
• version? : Option String

instance Lean.Lsp.instToJsonServerInfo : Lean.ToJson Lean.Lsp.ServerInfo

Equations

• Lean.Lsp.instToJsonServerInfo = { toJson := Lean.Lsp.toJsonServerInfo✝ }

instance Lean.Lsp.instFromJsonServerInfo : Lean.FromJson Lean.Lsp.ServerInfo

Equations

• Lean.Lsp.instFromJsonServerInfo = { fromJson? := Lean.Lsp.fromJsonServerInfo✝ }

structure Lean.Lsp.InitializeResult : Type

• capabilities : Lean.Lsp.ServerCapabilities
• serverInfo? : Option Lean.Lsp.ServerInfo

instance Lean.Lsp.instToJsonInitializeResult : Lean.ToJson Lean.Lsp.InitializeResult

Equations

• Lean.Lsp.instToJsonInitializeResult = { toJson := Lean.Lsp.toJsonInitializeResult✝ }

instance Lean.Lsp.instFromJsonInitializeResult : Lean.FromJson Lean.Lsp.InitializeResult

Equations

• Lean.Lsp.instFromJsonInitializeResult = { fromJson? := Lean.Lsp.fromJsonInitializeResult✝ }