-(* DESCRITTORI ESTERNI ALLA ALU *)
-
-(* getter della ALU, esiste sempre *)
-ndefinition get_alu ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.alu m t s.
-
-(* getter della memoria, esiste sempre *)
-ndefinition get_mem_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.mem_desc m t s.
-
-(* getter del descrittore, esiste sempre *)
-ndefinition get_chk_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.chk_desc m t s.
-
-(* getter del clik, esiste sempre *)
-ndefinition get_clk_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.clk_desc m t s.
-