Documentation

Lean.Data.Lsp.Client

structure Lean.Lsp.Registration:

Type

id : String
method : String
registerOptions : Option Lean.Json

instance Lean.Lsp.instToJsonRegistration:

Lean.ToJson Lean.Lsp.Registration

Equations

Lean.Lsp.instToJsonRegistration = { toJson := [anonymous] }

instance Lean.Lsp.instFromJsonRegistration:

Lean.FromJson Lean.Lsp.Registration

Equations

Lean.Lsp.instFromJsonRegistration = { fromJson? := [anonymous] }

structure Lean.Lsp.RegistrationParams:

Type

registrations : Array Lean.Lsp.Registration

instance Lean.Lsp.instToJsonRegistrationParams:

Lean.ToJson Lean.Lsp.RegistrationParams

Equations

Lean.Lsp.instToJsonRegistrationParams = { toJson := [anonymous] }

instance Lean.Lsp.instFromJsonRegistrationParams:

Lean.FromJson Lean.Lsp.RegistrationParams

Equations

Lean.Lsp.instFromJsonRegistrationParams = { fromJson? := [anonymous] }