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 := Lean.Lsp.toJsonRegistration✝ }

instance Lean.Lsp.instFromJsonRegistration : Lean.FromJson Lean.Lsp.Registration

Equations

• Lean.Lsp.instFromJsonRegistration = { fromJson? := Lean.Lsp.fromJsonRegistration✝ }

structure Lean.Lsp.RegistrationParams : Type

• registrations : Array Lean.Lsp.Registration

instance Lean.Lsp.instToJsonRegistrationParams : Lean.ToJson Lean.Lsp.RegistrationParams

instance Lean.Lsp.instFromJsonRegistrationParams : Lean.FromJson Lean.Lsp.RegistrationParams

Equations

• Lean.Lsp.instFromJsonRegistrationParams = { fromJson? := Lean.Lsp.fromJsonRegistrationParams✝ }