Defines Lean.Lsp.CancelParams.

This is separate from Lean.Data.Lsp.Basic to reduce transitive dependencies.

structure Lean.Lsp.CancelParams : Type

• id : JsonRpc.RequestID

def Lean.Lsp.instInhabitedCancelParams.default : CancelParams

Equations

• Lean.Lsp.instInhabitedCancelParams.default = { id := default }

instance Lean.Lsp.instInhabitedCancelParams : Inhabited CancelParams

Equations

• Lean.Lsp.instInhabitedCancelParams = { default := Lean.Lsp.instInhabitedCancelParams.default }

instance Lean.Lsp.instBEqCancelParams : BEq CancelParams

Equations

• Lean.Lsp.instBEqCancelParams = { beq := Lean.Lsp.instBEqCancelParams.beq }

def Lean.Lsp.instBEqCancelParams.beq : CancelParams → CancelParams → Bool

Equations

• Lean.Lsp.instBEqCancelParams.beq { id := a } { id := b } = (a == b)
• Lean.Lsp.instBEqCancelParams.beq x✝¹ x✝ = false

instance Lean.Lsp.instToJsonCancelParams : ToJson CancelParams

Equations

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

def Lean.Lsp.instToJsonCancelParams.toJson : CancelParams → Json

Equations

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

def Lean.Lsp.instFromJsonCancelParams.fromJson : Json → Except String CancelParams

Equations

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

instance Lean.Lsp.instFromJsonCancelParams : FromJson CancelParams

Equations

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