return λm:mcu_type.any_status m t → word32 → aux_mod_type → byte8 → option (any_status m t) with
[ HC05 ⇒ λs:any_status HC05 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
- (λmem.Some ? (set_mem_desc ? t s mem))
+ (λmem.Some ? (set_mem_desc ? t s mem))
| HC08 ⇒ λs:any_status HC08 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
(λmem.Some ? (set_mem_desc ? t s mem))
| HCS08 ⇒ λs:any_status HCS08 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
- (λmem.Some ? (set_mem_desc ? t s mem))
+ (λmem.Some ? (set_mem_desc ? t s mem))
| RS08 ⇒ λs:any_status RS08 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
RS08_memory_filter_write t s addr val
| IP2022 ⇒ λs:any_status IP2022 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
return λm:mcu_type.any_status m t → word32 → oct → bool → option (any_status m t) with
[ HC05 ⇒ λs:any_status HC05 t.λaddr:word32.λsub:oct.λval:bool.
opt_map … (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
- (λmem.Some ? (set_mem_desc ? t s mem))
+ (λmem.Some ? (set_mem_desc ? t s mem))
| HC08 ⇒ λs:any_status HC08 t.λaddr:word32.λsub:oct.λval:bool.
opt_map … (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
- (λmem.Some ? (set_mem_desc ? t s mem))
+ (λmem.Some ? (set_mem_desc ? t s mem))
| HCS08 ⇒ λs:any_status HCS08 t.λaddr:word32.λsub:oct.λval:bool.
opt_map … (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
(λmem.Some ? (set_mem_desc ? t s mem))