mod change (-x)

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

diff --git a/helm/software/matita/contribs/ng_assembly/num/word24.ma b/helm/software/matita/contribs/ng_assembly/num/word24.ma
old mode 100755 (executable)
new mode 100644 (file)
index 9495424..4aabde7
--- 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.