inductive MessageType : Type

• error : MessageType
• warning : MessageType
• info : MessageType
• log : MessageType

instance instFromJsonMessageType : Lean.FromJson MessageType

Equations

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

instance instToJsonMessageType : Lean.ToJson MessageType

Equations

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

structure ShowMessageParams : Type

• type : MessageType
• message : String

instance instFromJsonShowMessageParams : Lean.FromJson ShowMessageParams

Equations

• instFromJsonShowMessageParams = { fromJson? := fromJsonShowMessageParams✝ }

instance instToJsonShowMessageParams : Lean.ToJson ShowMessageParams

Equations

• instToJsonShowMessageParams = { toJson := toJsonShowMessageParams✝ }

structure MessageActionItem : Type

• title : String

instance instFromJsonMessageActionItem : Lean.FromJson MessageActionItem

Equations

• instFromJsonMessageActionItem = { fromJson? := fromJsonMessageActionItem✝ }

instance instToJsonMessageActionItem : Lean.ToJson MessageActionItem

Equations

• instToJsonMessageActionItem = { toJson := toJsonMessageActionItem✝ }

structure ShowMessageRequestParams : Type

• type : MessageType
• message : String
• actions? : Option (Array MessageActionItem)

instance instFromJsonShowMessageRequestParams : Lean.FromJson ShowMessageRequestParams

Equations

• instFromJsonShowMessageRequestParams = { fromJson? := fromJsonShowMessageRequestParams✝ }

instance instToJsonShowMessageRequestParams : Lean.ToJson ShowMessageRequestParams

Equations

• instToJsonShowMessageRequestParams = { toJson := toJsonShowMessageRequestParams✝ }

def ShowMessageResponse : Type

Equations

• ShowMessageResponse = Option MessageActionItem

instance instShowMessageResponseFromJson : Lean.FromJson ShowMessageResponse

Equations

• instShowMessageResponseFromJson = Lean.instFromJsonOption

instance instShowMessageResponseToJson : Lean.ToJson ShowMessageResponse

Equations

• instShowMessageResponseToJson = Lean.instToJsonOption