]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/ng_assembly/common/nat_to_num.ma
mod change (-x)
[helm.git] / helm / software / matita / contribs / ng_assembly / common / nat_to_num.ma
old mode 100755 (executable)
new mode 100644 (file)
index 6bd7fc4..f93f82e
@@ -75,4 +75,4 @@ nlet rec nat_of_w16_aux n (r:rec_word16 n) on r : nat ≝
 
 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.(nat65536 * (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)).