inductive t_byte8 (m:mcu_type) : Type ≝
TByte : byte8 → t_byte8 m.
-coercion cic:/matita/freescale/translation/t_byte8.ind#xpointer(1/1/1).
+coercion TByte.
(* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
inductive MA_check : instr_mode → Type ≝
inductive instruction : Type ≝
instr: ∀i:instr_mode.opcode → MA_check i → instruction.
-coercion cic:/matita/freescale/translation/instruction.ind#xpointer(1/1/1).
+coercion instr.
(* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
MA_check i → list (t_byte8 m) *)