structure Lean.Lsp.Registration : Type

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

Instances For

• Lean.Lsp.instFromJsonRegistration
• Lean.Lsp.instToJsonRegistration

instance Lean.Lsp.instToJsonRegistration : ToJson Registration

Equations

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

instance Lean.Lsp.instFromJsonRegistration : FromJson Registration

Equations

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

structure Lean.Lsp.RegistrationParams : Type

• registrations : Array Registration

Instances For

• Lean.Lsp.instFromJsonRegistrationParams
• Lean.Lsp.instToJsonRegistrationParams

instance Lean.Lsp.instToJsonRegistrationParams : ToJson RegistrationParams

Equations

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

instance Lean.Lsp.instFromJsonRegistrationParams : FromJson RegistrationParams

Equations

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