X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fexadecim.ma;h=62de47a89eb50603f63def979c402ab6f0c385e3;hb=b886a562ccbfc3f63b8f64a135bcf70e4b189999;hp=b0c0faf197fe5a945194ebe0cca03414bafe5db1;hpb=be0ca791abbf1084b7218f2d17ab48462fbb3049;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
index b0c0faf19..62de47a89 100755
--- a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/exadecim.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                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -713,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:nat) on n ≝
- match n with
-  [ O ⇒ e
-  | S n' ⇒ ror_ex_n (ror_ex e) n' ].
+nlet rec ror_ex_n (e:exadecim) (q:quatern) (rq:rec_quatern q) on rq ≝
+ match rq with
+  [ qu_O ⇒ e
+  | qu_S q' n' ⇒ ror_ex_n (ror_ex e) q' n' ].
 
 (* operatore rotazione sinistra con carry *)
 ndefinition rcl_ex ≝
@@ -762,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:nat) on n ≝
- match n with
-  [ O ⇒ e
-  | S n' ⇒ rol_ex_n (rol_ex e) n' ].
+nlet rec rol_ex_n (e:exadecim) (q:quatern) (rq:rec_quatern q) on rq ≝
+ match rq with
+  [ qu_O ⇒ e
+  | qu_S q' n' ⇒ rol_ex_n (rol_ex e) q' n' ].
 
 (* operatore not/complemento a 1 *)
 ndefinition not_ex ≝
@@ -1378,6 +1378,13 @@ ndefinition compl_ex ≝
  | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
  | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
 
+(* operatore x in [inf,sup] o in sup],[inf *)
+ndefinition inrange_ex ≝
+λx,inf,sup:exadecim.
+ match le_ex inf sup with
+  [ true ⇒ and_bool | false ⇒ or_bool ]
+ (le_ex inf x) (le_ex x sup).
+
 (* iteratore sugli esadecimali *)
 ndefinition forall_ex ≝ λP.
  P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗