source
structure Lean.Lsp.Registration :
Type

- id : String
- method : String
- registerOptions : Option Json

Instances For

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

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

Instances For

source
instance Lean.Lsp.instToJsonRegistration :
ToJson Registration
Equations

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

source
instance Lean.Lsp.instFromJsonRegistration :
FromJson Registration
Equations

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

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

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

Instances For

source
structure Lean.Lsp.RegistrationParams :
Type

- registrations : Array Registration

Instances For

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

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

Instances For

source
instance Lean.Lsp.instToJsonRegistrationParams :
ToJson RegistrationParams
Equations

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

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

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

Instances For

source
instance Lean.Lsp.instFromJsonRegistrationParams :
FromJson RegistrationParams
Equations

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