| IP2022 ⇒ IP2022_multi_mode_load_auxw
].
-(* tutte le modalita' di lettura: false=loadb true=loadw *)
-
(* **************************************** *)
(* raccordo di tutte le possibili scritture *)
(* **************************************** *)
ndefinition multi_mode_writeb ≝
λm.match m
- return λm.Πt.any_status m t → word16 → aux_im_type m → byte8 →
+ return λm.Πt.any_status m t → word16 → aux_mod_type → aux_im_type m → byte8 →
option (ProdT (any_status m t) word16)
with
[ HC05 ⇒ Freescale_multi_mode_write_auxb HC05