X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fbyte8.ma;h=9cf490eab98a439913e5659bc647ca30589a5787;hb=eb4144a401147a44a9620169eb6dafeb8f5a2c17;hp=b2ad856f0e1f0fc09b8918a19dd2273b969fff96;hpb=6ee4fa0ba5f4b6601b62afd482d4f30bd2de2f91;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8.ma b/helm/software/matita/contribs/ng_assembly/num/byte8.ma
index b2ad856f0..9cf490eab 100755
--- a/helm/software/matita/contribs/ng_assembly/num/byte8.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/byte8.ma
@@ -71,6 +71,14 @@ ndefinition setMSB_b8 ≝ setOPH_cn ? setMSB_ex.
 ndefinition getLSB_b8 ≝ getOPL_cn ? getLSB_ex.
 ndefinition setLSB_b8 ≝ setOPL_cn ? setLSB_ex.
 
+(* operatore estensione unsigned *)
+ndefinition extu_b8 ≝ λe2.〈x0,e2〉.
+
+(* operatore estensione signed *)
+ndefinition exts_b8 ≝
+λe2.〈(match getMSB_ex e2 with 
+      [ true ⇒ xF | false ⇒ x0 ]),e2〉.
+
 (* operatore rotazione destra con carry *)
 ndefinition rcr_b8 ≝ opcr_cn ? rcr_ex.