(* ********************************************************************** *)
(* 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 *)
(* *)
(* ********************************************************************** *)
nlet rec nat_of_qu_aux n (r:rec_quatern n) on r ≝
match r with
- [ qu_O ⇒ 0
+ [ qu_O ⇒ O
| qu_S t n' ⇒ S (nat_of_qu_aux t n')
].
nlet rec nat_of_oct_aux n (r:rec_oct n) on r ≝
match r with
- [ oc_O ⇒ 0
+ [ oc_O ⇒ O
| oc_S t n' ⇒ S (nat_of_oct_aux t n')
].
nlet rec nat_of_ex_aux n (r:rec_exadecim n) on r ≝
match r with
- [ ex_O ⇒ 0
+ [ ex_O ⇒ O
| ex_S t n' ⇒ S (nat_of_ex_aux t n')
].
nlet rec nat_of_bit_aux n (r:rec_bitrigesim n) on r ≝
match r with
- [ bi_O ⇒ 0
+ [ bi_O ⇒ O
| bi_S t n' ⇒ S (nat_of_bit_aux t n')
].
nlet rec nat_of_b8_aux n (r:rec_byte8 n) on r ≝
match r with
- [ b8_O ⇒ 0
+ [ b8_O ⇒ O
| b8_S t n' ⇒ S (nat_of_b8_aux t n')
].
nlet rec nat_of_w16_aux n (r:rec_word16 n) on r : nat ≝
match r with
- [ w16_O ⇒ 0
+ [ w16_O ⇒ O
| w16_S t n' ⇒ S (nat_of_w16_aux t n')
].
ndefinition nat_of_w16 : word16 → nat ≝ λn:word16.nat_of_w16_aux n (w16_to_recw16 n).
-ndefinition nat_of_w32 : word32 → nat ≝ λn:word32.(256*256*(nat_of_w16 (w32h n))) + (nat_of_w16 (w32l n)).
+ndefinition nat_of_w32 : word32 → nat ≝ λn:word32.(nat65536 * (nat_of_w16 (w32h n))) + (nat_of_w16 (w32l n)).