Defines Lean.Lsp.CancelParams.

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

structure Lean.Lsp.CancelParams : Type

• id : JsonRpc.RequestID

instance Lean.Lsp.instInhabitedCancelParams : Inhabited CancelParams

Equations

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

instance Lean.Lsp.instBEqCancelParams : BEq CancelParams

Equations

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

instance Lean.Lsp.instToJsonCancelParams : ToJson CancelParams

Equations

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

instance Lean.Lsp.instFromJsonCancelParams : FromJson CancelParams

Equations

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