ndefinition word16 ≝ comp_num byte8.
ndefinition mk_word16 ≝ λb1,b2.mk_comp_num byte8 b1 b2.
+ndefinition ext_word16 ≝ λb2.mk_comp_num byte8 〈x0,x0〉 b2.
+ndefinition ext2_word16 ≝ λe2.mk_comp_num byte8 〈x0,x0〉 〈x0,e2〉.
(* \langle \rangle *)
notation "〈x:y〉" non associative with precedence 80
ndefinition getLSB_w16 ≝ getOPL_cn ? getLSB_b8.
ndefinition setLSB_w16 ≝ setOPL_cn ? setLSB_b8.
+(* operatore estensione unsigned *)
+ndefinition extu_w16 ≝ λb2.〈〈x0,x0〉:b2〉.
+ndefinition extu2_w16 ≝ λe2.〈〈x0,x0〉:〈x0,e2〉〉.
+
+(* operatore estensione signed *)
+ndefinition exts_w16 ≝
+λb2.〈(match getMSB_b8 b2 with
+ [ true ⇒ 〈xF,xF〉 | false ⇒ 〈x0,x0〉 ]):b2〉.
+ndefinition exts2_w16 ≝
+λe2.(match getMSB_ex e2 with
+ [ true ⇒ 〈〈xF,xF〉:〈xF,e2〉〉 | false ⇒ 〈〈x0,x0〉:〈x0,e2〉〉 ]).
+
(* operatore rotazione destra con carry *)
ndefinition rcr_w16 ≝ opcr_cn ? rcr_b8.