inductive Lean.Lsp.MessageType : Type

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

@[instance_reducible]

instance Lean.Lsp.instFromJsonMessageType : FromJson MessageType

Equations

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

@[instance_reducible]

instance Lean.Lsp.instToJsonMessageType : ToJson MessageType

Equations

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

structure Lean.Lsp.ShowMessageParams : Type

• type : MessageType
• message : String

@[instance_reducible]

instance Lean.Lsp.instFromJsonShowMessageParams : FromJson ShowMessageParams

Equations

• Lean.Lsp.instFromJsonShowMessageParams = { fromJson? := Lean.Lsp.instFromJsonShowMessageParams.fromJson }

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

Equations

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

@[instance_reducible]

instance Lean.Lsp.instToJsonShowMessageParams : ToJson ShowMessageParams

Equations

• Lean.Lsp.instToJsonShowMessageParams = { toJson := Lean.Lsp.instToJsonShowMessageParams.toJson }

def Lean.Lsp.instToJsonShowMessageParams.toJson : ShowMessageParams → Json

Equations

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

structure Lean.Lsp.MessageActionItem : Type

• title : String

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

Equations

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

@[instance_reducible]

instance Lean.Lsp.instFromJsonMessageActionItem : FromJson MessageActionItem

Equations

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

def Lean.Lsp.instToJsonMessageActionItem.toJson : MessageActionItem → Json

Equations

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

@[instance_reducible]

instance Lean.Lsp.instToJsonMessageActionItem : ToJson MessageActionItem

Equations

• Lean.Lsp.instToJsonMessageActionItem = { toJson := Lean.Lsp.instToJsonMessageActionItem.toJson }

structure Lean.Lsp.ShowMessageRequestParams : Type

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

@[instance_reducible]

instance Lean.Lsp.instFromJsonShowMessageRequestParams : FromJson ShowMessageRequestParams

Equations

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

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

Equations

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

def Lean.Lsp.instToJsonShowMessageRequestParams.toJson : ShowMessageRequestParams → Json

Equations

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

@[instance_reducible]

instance Lean.Lsp.instToJsonShowMessageRequestParams : ToJson ShowMessageRequestParams

Equations

• Lean.Lsp.instToJsonShowMessageRequestParams = { toJson := Lean.Lsp.instToJsonShowMessageRequestParams.toJson }

def Lean.Lsp.ShowMessageResponse : Type

Equations

• Lean.Lsp.ShowMessageResponse = Option Lean.Lsp.MessageActionItem

@[instance_reducible]

instance Lean.Lsp.instFromJsonShowMessageResponse : FromJson ShowMessageResponse

Equations

• Lean.Lsp.instFromJsonShowMessageResponse = { fromJson? := Lean.Lsp.instFromJsonShowMessageResponse._aux_1 }

@[instance_reducible]

instance Lean.Lsp.instToJsonShowMessageResponse : ToJson ShowMessageResponse

Equations

• Lean.Lsp.instToJsonShowMessageResponse = { toJson := Lean.Lsp.instToJsonShowMessageResponse._aux_1 }