structure Lean.Lsp.Registration : Type

• id : String
• method : String
• registerOptions : Option Json

instance Lean.Lsp.instToJsonRegistration : ToJson Registration

Equations

• Lean.Lsp.instToJsonRegistration = { toJson := Lean.Lsp.instToJsonRegistration.toJson }

def Lean.Lsp.instToJsonRegistration.toJson : Registration → Json

Equations

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

instance Lean.Lsp.instFromJsonRegistration : FromJson Registration

Equations

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

def Lean.Lsp.instFromJsonRegistration.fromJson : Json → Except String Registration

Equations

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

structure Lean.Lsp.RegistrationParams : Type

• registrations : Array Registration

def Lean.Lsp.instToJsonRegistrationParams.toJson : RegistrationParams → Json

Equations

• Lean.Lsp.instToJsonRegistrationParams.toJson x✝ = Lean.Json.mkObj [[("registrations", Lean.toJson x✝.registrations)]].flatten

instance Lean.Lsp.instToJsonRegistrationParams : ToJson RegistrationParams

Equations

• Lean.Lsp.instToJsonRegistrationParams = { toJson := Lean.Lsp.instToJsonRegistrationParams.toJson }

def Lean.Lsp.instFromJsonRegistrationParams.fromJson : Json → Except String RegistrationParams

Equations

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

instance Lean.Lsp.instFromJsonRegistrationParams : FromJson RegistrationParams

Equations

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