∀ (method : String) (direction : Lean.JsonRpc.MessageDirection)
  (kinds : Array Lean.Server.Overview.ProtocolExtensionKind✝) (parameterType : Type) (description : String),
  sizeOf
      { method := method, direction := direction, kinds := kinds, parameterType := parameterType,
        description := description } =
    1 + sizeOf method + sizeOf direction + sizeOf kinds + sizeOf parameterType + sizeOf description