freescale porting

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

diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8.ma b/helm/software/matita/contribs/ng_assembly/num/byte8.ma
index b2ad856f0e1f0fc09b8918a19dd2273b969fff96..9cf490eab98a439913e5659bc647ca30589a5787 100755 (executable)
--- 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.