(* pc word aligned, mappato in 0x02000000-0x0201FFFF *)
ndefinition IP2022_fetch_byte_or_word ≝
λm:mcu_type.λfR:word32 → option byte8.λpc:word16.
(* pc word aligned, mappato in 0x02000000-0x0201FFFF *)
ndefinition IP2022_fetch_byte_or_word ≝
λm:mcu_type.λfR:word32 → option byte8.λpc:word16.