max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove dangerous instances in json-rpc

Browse source
This commit is contained in:
Gabriel Ebner 2022-12-05 19:31:23 -08:00
parent 434d889f4d
commit 118567657d
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Data/JsonRpc.lean
View file

@ -127,7 +127,7 @@ structure Request (α : Type u) where
param : α
deriving Inhabited, BEq
instance [ToJson α] : Coe (Request α) Message :=
instance [ToJson α] : CoeHead (Request α) Message :=
⟨fun r => Message.request r.id r.method (toStructured? r.param).toOption⟩
/-- Generic version of `Message.notification`.
@ -142,7 +142,7 @@ structure Notification (α : Type u) where
param : α
deriving Inhabited, BEq
instance [ToJson α] : Coe (Notification α) Message :=
instance [ToJson α] : CoeHead (Notification α) Message :=
⟨fun r => Message.notification r.method (toStructured? r.param).toOption⟩
/-- Generic version of `Message.response`.
@ -161,7 +161,7 @@ structure Response (α : Type u) where
result : α
deriving Inhabited, BEq
instance [ToJson α] : Coe (Response α) Message :=
instance [ToJson α] : CoeHead (Response α) Message :=
⟨fun r => Message.response r.id (toJson r.result)⟩
/-- Generic version of `Message.responseError`.
@ -180,7 +180,7 @@ structure ResponseError (α : Type u) where
data? : Option α := none
deriving Inhabited, BEq
instance [ToJson α] : Coe (ResponseError α) Message :=
instance [ToJson α] : CoeHead (ResponseError α) Message :=
⟨fun r => Message.responseError r.id r.code r.message (r.data?.map toJson)⟩
instance : Coe String RequestID := ⟨RequestID.str⟩