source
inductive MessageType :
Type

- error : MessageType
- warning : MessageType
- info : MessageType
- log : MessageType

Instances For

source
instance instFromJsonMessageType :
Lean.FromJson MessageType
Equations

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

source
instance instToJsonMessageType :
Lean.ToJson MessageType
Equations

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

source
structure ShowMessageParams :
Type

- type : MessageType
- message : String

Instances For

source
instance instFromJsonShowMessageParams :
Lean.FromJson ShowMessageParams
Equations

- instFromJsonShowMessageParams = { fromJson? := instFromJsonShowMessageParams.fromJson }

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

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

Instances For

source
instance instToJsonShowMessageParams :
Lean.ToJson ShowMessageParams
Equations

- instToJsonShowMessageParams = { toJson := instToJsonShowMessageParams.toJson }

source
def instToJsonShowMessageParams.toJson :
ShowMessageParams → Lean.Json
Equations

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

Instances For

source
structure MessageActionItem :
Type

- title : String

Instances For

source
instance instFromJsonMessageActionItem :
Lean.FromJson MessageActionItem
Equations

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

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

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

Instances For

source
instance instToJsonMessageActionItem :
Lean.ToJson MessageActionItem
Equations

- instToJsonMessageActionItem = { toJson := instToJsonMessageActionItem.toJson }

source
def instToJsonMessageActionItem.toJson :
MessageActionItem → Lean.Json
Equations

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

Instances For

source
structure ShowMessageRequestParams :
Type

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

Instances For

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

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

Instances For

source
instance instFromJsonShowMessageRequestParams :
Lean.FromJson ShowMessageRequestParams
Equations

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

source
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

Instances For

source
instance instToJsonShowMessageRequestParams :
Lean.ToJson ShowMessageRequestParams
Equations

- instToJsonShowMessageRequestParams = { toJson := instToJsonShowMessageRequestParams.toJson }

source
def ShowMessageResponse :
Type
Equations

- ShowMessageResponse = Option MessageActionItem

Instances For

source
instance instFromJsonShowMessageResponse :
Lean.FromJson ShowMessageResponse
Equations

- instFromJsonShowMessageResponse = Lean.instFromJsonOption

source
instance instToJsonShowMessageResponse :
Lean.ToJson ShowMessageResponse
Equations

- instToJsonShowMessageResponse = Lean.instToJsonOption