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? := instFromJsonShowMessageParams.fromJson }

def instFromJsonShowMessageParams.fromJson : Lean.Json → Except String ShowMessageParams

Equations

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

instance instToJsonShowMessageParams : Lean.ToJson ShowMessageParams

Equations

• instToJsonShowMessageParams = { toJson := instToJsonShowMessageParams.toJson }

def instToJsonShowMessageParams.toJson : ShowMessageParams → Lean.Json

Equations

• instToJsonShowMessageParams.toJson x✝ = Lean.Json.mkObj [[("type", Lean.toJson x✝.type)], [("message", Lean.toJson x✝.message)]].flatten

structure MessageActionItem : Type

• title : String

def instFromJsonMessageActionItem.fromJson : Lean.Json → Except String MessageActionItem

Equations

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

instance instFromJsonMessageActionItem : Lean.FromJson MessageActionItem

Equations

• instFromJsonMessageActionItem = { fromJson? := instFromJsonMessageActionItem.fromJson }

def instToJsonMessageActionItem.toJson : MessageActionItem → Lean.Json

Equations

• instToJsonMessageActionItem.toJson x✝ = Lean.Json.mkObj [[("title", Lean.toJson x✝.title)]].flatten

instance instToJsonMessageActionItem : Lean.ToJson MessageActionItem

Equations

• instToJsonMessageActionItem = { toJson := instToJsonMessageActionItem.toJson }

structure ShowMessageRequestParams : Type

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

def instFromJsonShowMessageRequestParams.fromJson : Lean.Json → Except String ShowMessageRequestParams

Equations

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

instance instFromJsonShowMessageRequestParams : Lean.FromJson ShowMessageRequestParams

Equations

• instFromJsonShowMessageRequestParams = { fromJson? := instFromJsonShowMessageRequestParams.fromJson }

def instToJsonShowMessageRequestParams.toJson : ShowMessageRequestParams → Lean.Json

Equations

• instToJsonShowMessageRequestParams.toJson x✝ = Lean.Json.mkObj [[("type", Lean.toJson x✝.type)], [("message", Lean.toJson x✝.message)], Lean.Json.opt "actions" x✝.actions?].flatten

instance instToJsonShowMessageRequestParams : Lean.ToJson ShowMessageRequestParams

Equations

• instToJsonShowMessageRequestParams = { toJson := instToJsonShowMessageRequestParams.toJson }

def ShowMessageResponse : Type

Equations

• ShowMessageResponse = Option MessageActionItem

instance instFromJsonShowMessageResponse : Lean.FromJson ShowMessageResponse

Equations

• instFromJsonShowMessageResponse = Lean.instFromJsonOption

instance instToJsonShowMessageResponse : Lean.ToJson ShowMessageResponse

Equations

• instToJsonShowMessageResponse = Lean.instToJsonOption