(* ********************************************************************** *)
(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Ultima modifica: 05/08/2009 *)
(* *)
(* ********************************************************************** *)
include "freescale/memory_struct.ma".
-include "freescale/word16.ma".
-include "freescale/option.ma".
-include "freescale/theory.ma".
+include "num/word16.ma".
+include "common/option.ma".
+include "common/list.ma".
(* ********************* *)
(* MEMORIA E DESCRITTORE *)
(* (mf_check_update_ranged chk inf sup mode) = setta tipo memoria *)
ndefinition mf_check_update_ranged ≝
λf:word16 → memory_type.λi.λs.λv.
- λx.match in_range x i s with
+ λx.match inrange_w16 x i s with
[ true ⇒ v
| false ⇒ f x ].