freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / num / exadecim.ma

diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
index 10019b37920956383f5e148294d9ac6b9047bb23..b0c0faf197fe5a945194ebe0cca03414bafe5db1 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
@@ -24,6 +24,7 @@ include "num/bool.ma".
 include "num/quatern.ma".
 include "num/oct.ma".
 include "common/prod.ma".
+include "common/nat.ma".
 
 (* *********** *)
 (* ESADECIMALI *)
@@ -712,10 +713,10 @@ ndefinition ror_ex ≝
  | xC ⇒ x6 | xD ⇒ xE | xE ⇒ x7 | xF ⇒ xF ].
 
 (* operatore rotazione destra n-volte *)
-nlet rec ror_ex_n (e:exadecim) (n:quatern) (r:rec_quatern n) on r ≝
- match r with
-  [ qu_O ⇒ e
-  | qu_S t n' ⇒ ror_ex_n (ror_ex e) t n' ].
+nlet rec ror_ex_n (e:exadecim) (n:nat) on n ≝
+ match n with
+  [ O ⇒ e
+  | S n' ⇒ ror_ex_n (ror_ex e) n' ].
 
 (* operatore rotazione sinistra con carry *)
 ndefinition rcl_ex ≝
@@ -761,10 +762,10 @@ ndefinition rol_ex ≝
  | xC ⇒ x9 | xD ⇒ xB | xE ⇒ xD | xF ⇒ xF ].
 
 (* operatore rotazione sinistra n-volte *)
-nlet rec rol_ex_n (e:exadecim) (n:quatern) (r:rec_quatern n) on r ≝
- match r with
-  [ qu_O ⇒ e
-  | qu_S t n' ⇒ rol_ex_n (rol_ex e) t n' ].
+nlet rec rol_ex_n (e:exadecim) (n:nat) on n ≝
+ match n with
+  [ O ⇒ e
+  | S n' ⇒ rol_ex_n (rol_ex e) n' ].
 
 (* operatore not/complemento a 1 *)
 ndefinition not_ex ≝