X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fword24.ma;h=4aabde7710cf2124ca4eb7be29a96344acff3a4c;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=94954244b3e447ac767417c6e2ef91546401ed98;hpb=6ee4fa0ba5f4b6601b62afd482d4f30bd2de2f91;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/num/word24.ma b/helm/software/matita/contribs/ng_assembly/num/word24.ma
index 94954244b..4aabde771 100755
--- a/helm/software/matita/contribs/ng_assembly/num/word24.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word24.ma
@@ -104,10 +104,12 @@ ndefinition xor_w24 ≝
 (* operatore Most Significant Bit *)
 ndefinition getMSB_w24 ≝ λw:word24.getMSB_b8 (w24x w).
 ndefinition setMSB_w24 ≝ λw:word24.mk_word24 (setMSB_b8 (w24x w)) (w24h w) (w24l w).
+ndefinition clrMSB_w24 ≝ λw:word24.mk_word24 (clrMSB_b8 (w24x w)) (w24h w) (w24l w).
 
 (* operatore Least Significant Bit *)
 ndefinition getLSB_w24 ≝ λw:word24.getLSB_b8 (w24l w).
 ndefinition setLSB_w24 ≝ λw:word24.mk_word24 (w24x w) (w24h w) (setLSB_b8 (w24l w)).
+ndefinition clrLSB_w24 ≝ λw:word24.mk_word24 (w24x w) (w24h w) (clrLSB_b8 (w24l w)).
 
 (* operatore rotazione destra con carry *)
 ndefinition rcr_w24 ≝
@@ -190,6 +192,11 @@ ndefinition compl_w24 ≝
  [ true ⇒ succ_w24 (not_w24 w)
  | false ⇒ not_w24 (pred_w24 w) ].
 
+(* operatore abs *)
+ndefinition abs_w24 ≝
+λw:word24.match getMSB_w24 w with
+ [ true ⇒ compl_w24 w | false ⇒ w ].
+
 (* operatore x in [inf,sup] o in sup],[inf *)
 ndefinition inrange_w24 ≝
 λx,inf,sup:word24.