Apparent problem with DMA details in device file MK20DX256.h

Hi, I have been hard at work writing a device driver library for the SGTL5000 using the Teensy3.2. The Teensy is using the MK20DX256 mcu and I think there is a little issue with the device file for this device inside the mbed library. File: MK20DX256.h

Specifically the DMA channels (All 16 of them!) can have a channel priority programmed. The MK20DX256 reference manual specifically refers to all 16 channels having programmable priority. Indeed I have bit banged these fields in accordance with the reference manual and they are writable and seem to work. However the device file seems only to refer to channels 0-3. This makes it rather awkward to program these priorities effectively.

The device file struct is as follows:
__IO uint8_t DCHPRI3; /< Channel n Priority Register, offset: 0x100 */
__IO uint8_t DCHPRI2; /
< Channel n Priority Register, offset: 0x101 */
__IO uint8_t DCHPRI1; /< Channel n Priority Register, offset: 0x102 */
__IO uint8_t DCHPRI0; /
< Channel n Priority Register, offset: 0x103 */

Where are the other channels.

I believe it should as a minimum look like this:
__IO uint8_t DCHPRI3; /< Channel n Priority Register, offset: 0x100 */
__IO uint8_t DCHPRI2; /
< Channel n Priority Register, offset: 0x101 */
__IO uint8_t DCHPRI1; /< Channel n Priority Register, offset: 0x102 */
__IO uint8_t DCHPRI0; /
< Channel n Priority Register, offset: 0x103 */
__IO uint8_t DCHPRI7; /< Channel n Priority Register, offset: 0x104 */
__IO uint8_t DCHPRI6; /
< Channel n Priority Register, offset: 0x105 */
__IO uint8_t DCHPRI5; /< Channel n Priority Register, offset: 0x106 */
__IO uint8_t DCHPRI4; /
< Channel n Priority Register, offset: 0x107 */
__IO uint8_t DCHPRI11; /< Channel n Priority Register, offset: 0x108 */
__IO uint8_t DCHPRI10; /
< Channel n Priority Register, offset: 0x109 */
__IO uint8_t DCHPRI9; /< Channel n Priority Register, offset: 0x10A */
__IO uint8_t DCHPRI8; /
< Channel n Priority Register, offset: 0x10B */
__IO uint8_t DCHPRI15; /< Channel n Priority Register, offset: 0x10C */
__IO uint8_t DCHPRI14; /
< Channel n Priority Register, offset: 0x10D */
__IO uint8_t DCHPRI13; /< Channel n Priority Register, offset: 0x10E */
__IO uint8_t DCHPRI12; /
< Channel n Priority Register, offset: 0x10F */

Better still would be to allow array style indexing, otherwise it difficult to programatically reference these values.

I see the file originated from Freescale, Perhaps I have not fully understood the methodology. But I am happily using all 16 channels. I have checked the reset values of each channel, and it is as documented. I have programmed different priorities in channels not defined, and all seem well.

FYI.
Regards