(* scrittura su [byte [curpc]]: true=DIR1 writeb, false=DIR1 writew *)
ndefinition mode_DIR1_write ≝
λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].
(* scrittura su [byte [curpc]]: true=DIR1 writeb, false=DIR1 writew *)
ndefinition mode_DIR1_write ≝
λbyteflag:bool.λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.
λwritebw:match byteflag with [ true ⇒ byte8 | false ⇒ word16 ].