instRpcEncodableSelectInsertParams

Lean4
instance : RpcEncodable✝ (@SelectInsertParams✝) :=
  { rpcEncode✝ := enc✝, rpcDecode✝ := dec✝ }
where
   enc✝ a✝ :=
    return
      toJson✝
        { pos := ← rpcEncode✝ a✝.pos, goals := ← rpcEncode✝ a✝.goals,
          selectedLocations := ← rpcEncode✝ a✝.selectedLocations, replaceRange := ← rpcEncode✝ a✝.replaceRange :
          RpcEncodablePacket✝ }
   dec✝ j✝ := do
    let a✝ : RpcEncodablePacket✝ ← fromJson?✝ j✝
    return
      { pos := ← rpcDecode✝ a✝.pos, goals := ← rpcDecode✝ a✝.goals,
        selectedLocations := ← rpcDecode✝ a✝.selectedLocations, replaceRange := ← rpcDecode✝ a✝.replaceRange }
Похожие утверждения