(* \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)).