ndefinition multi_mode_loadb ≝
λm.match m
- return λm.Πt.any_status m t → word16 → word16 → aux_im_type m →
+ return λm.Πt.any_status m t → word16 → aux_im_type m →
option (Prod3T (any_status m t) byte8 word16)
with
[ HC05 ⇒ Freescale_multi_mode_load_auxb HC05
ndefinition multi_mode_loadw ≝
λm.match m
- return λm.Πt.any_status m t → word16 → word16 → aux_im_type m →
+ return λm.Πt.any_status m t → word16 → aux_im_type m →
option (Prod3T (any_status m t) word16 word16)
with
[ HC05 ⇒ Freescale_multi_mode_load_auxw HC05
| 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 → word16 → aux_mod_type → 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
ndefinition multi_mode_writew ≝
λm.match m
- return λm.Πt.any_status m t → word16 → word16 → aux_im_type m → word16 →
+ return λm.Πt.any_status m t → word16 → aux_im_type m → word16 →
option (ProdT (any_status m t) word16)
with
[ HC05 ⇒ Freescale_multi_mode_write_auxw HC05