(* \langle \rangle *)
notation "〈x:y〉" non associative with precedence 80
for @{ 'mk_word16 $x $y }.
-interpretation "mk_word16" 'mk_word16 x y =
- (cic:/matita/freescale/word16/word16.ind#xpointer(1/1/1) x y).
+interpretation "mk_word16" 'mk_word16 x y = (mk_word16 x y).
(* operatore = *)
definition eq_w16 ≝ λw1,w2.(eq_b8 (w16h w1) (w16h w2)) ⊗ (eq_b8 (w16l w1) (w16l w2)).
(* word → naturali *)
definition nat_of_word16 ≝ λw:word16. 256 * (w16h w) + (nat_of_byte8 (w16l w)).
-coercion cic:/matita/freescale/word16/nat_of_word16.con.
+coercion nat_of_word16.
(* naturali → word *)
definition word16_of_nat ≝