(* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
MA_check i → list (t_byte8 m) *)
ndefinition IP2022_args_picker ≝
-λi:aux_im_type IP2022.λargs:IP2022_MA_check i.
+λi:IP2022_instr_mode.λargs:IP2022_MA_check i.
match args with
[ maINH ⇒ nil ?
| maIMM3 _ ⇒ nil ?