X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fexadecim.ma;h=1951578a4e656ce477c48f2843eaba6f37649f83;hb=e7264f953fcf2cd2bef9057d83add08996d2ce75;hp=07c19464a70071a8c912395723796e702bd6be8f;hpb=b082cb1e1fc9dbd471d16d2eb231e883e96e588f;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 07c19464a..1951578a4 100755
--- a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
@@ -688,6 +688,13 @@ ndefinition setMSB_ex ≝
  | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
  | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ].
 
+ndefinition clrMSB_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
+ | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
+ | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
+ | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ].
+
 (* operatore Least Significant Bit *)
 ndefinition getLSB_ex ≝
 λe:exadecim.match e with
@@ -703,6 +710,13 @@ ndefinition setLSB_ex ≝
  | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
  | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ].
 
+ndefinition clrLSB_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
+ | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
+ | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
+ | xC ⇒ xC | xD ⇒ xC | xE ⇒ xE | xF ⇒ xE ].
+
 (* operatore rotazione destra con carry *)
 ndefinition rcr_ex ≝
 λc:bool.λe:exadecim.match c with
@@ -1392,6 +1406,11 @@ ndefinition compl_ex ≝
  | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
  | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
 
+(* operatore abs *)
+ndefinition abs_ex ≝
+λe:exadecim.match getMSB_ex e with
+ [ true ⇒ compl_ex e | false ⇒ e ].
+
 (* operatore x in [inf,sup] o in sup],[inf *)
 ndefinition inrange_ex ≝
 λx,inf,sup:exadecim.