X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcommon%2Fnat_to_num.ma;h=f93f82e8d94674a395a4a8ec8734f58bdf55422f;hb=603f2f6b596d8632b9bd53c73ae0b9c3575231e0;hp=db38d086d6cffed404c9d95968ace9a7cdb9c7dc;hpb=20166e1ce9d14f6a3586a10d98ac3f1571207586;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/common/nat_to_num.ma b/helm/software/matita/contribs/ng_assembly/common/nat_to_num.ma
index db38d086d..f93f82e8d 100755
--- a/helm/software/matita/contribs/ng_assembly/common/nat_to_num.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/nat_to_num.ma
@@ -15,8 +15,8 @@
 (* ********************************************************************** *)
 (*                          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              *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -29,7 +29,7 @@ include "num/word32.ma".
 
 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')
   ].
 
@@ -37,7 +37,7 @@ ndefinition nat_of_qu : quatern → nat ≝ λn.nat_of_qu_aux n (qu_to_recqu 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')
   ].
 
@@ -45,7 +45,7 @@ ndefinition nat_of_oct : oct → nat ≝ λn.nat_of_oct_aux n (oct_to_recoct 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')
   ].
 
@@ -53,7 +53,7 @@ ndefinition nat_of_ex : exadecim → nat ≝ λn.nat_of_ex_aux n (ex_to_recex 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')
   ].
 
@@ -61,7 +61,7 @@ ndefinition nat_of_bit : bitrigesim → nat ≝ λn.nat_of_bit_aux n (bit_to_rec
 
 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')
   ].
 
@@ -69,10 +69,10 @@ ndefinition nat_of_b8 : byte8 → nat ≝ λn:byte8.nat_of_b8_aux n (b8_to_recb8
 
 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 (cnH ? n))) + (nat_of_w16 (cnL ? n)).