(* \langle \rangle *)
notation "〈x,y〉" non associative with precedence 80
for @{ 'mk_byte8 $x $y }.
-interpretation "mk_byte8" 'mk_byte8 x y =
- (cic:/matita/freescale/byte8/byte8.ind#xpointer(1/1/1) x y).
+interpretation "mk_byte8" 'mk_byte8 x y = (mk_byte8 x y).
(* operatore = *)
definition eq_b8 ≝ λb1,b2:byte8.(eq_ex (b8h b1) (b8h b2)) ⊗ (eq_ex (b8l b1) (b8l b2)).
(* byte → naturali *)
definition nat_of_byte8 ≝ λb:byte8.16*(b8h b) + (b8l b).
-coercion cic:/matita/freescale/byte8/nat_of_byte8.con.
+coercion nat_of_byte8.
(* naturali → byte *)
definition byte8_of_nat ≝ λn.mk_byte8 (exadecim_of_nat (n/16)) (exadecim_of_nat n).