instRpcEncodableCalcParams — Mathlib

Lean4
instance : RpcEncodable✝ (@CalcParams✝) :=
  { 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,
          isFirst := ← rpcEncode✝ a✝.isFirst, indent := ← rpcEncode✝ a✝.indent : 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,
        isFirst := ← rpcDecode✝ a✝.isFirst, indent := ← rpcDecode✝ a✝.indent }
Похожие утверждения