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] }