notation "〈x:y〉" non associative with precedence 80
for @{ mk_comp_num byte8 $x $y }.
+ndefinition word16_is_comparable ≝ cn_is_comparable byte8_is_comparable.
ndefinition word16_is_comparable_ext ≝ cn_is_comparable_ext byte8_is_comparable_ext.
unification hint 0 ≔ ⊢ carr (comp_base word16_is_comparable_ext) ≡ comp_num (comp_num exadecim).
unification hint 0 ≔ ⊢ carr (comp_base word16_is_comparable_ext) ≡ comp_num byte8.
unification hint 0 ≔ ⊢ carr (comp_base word16_is_comparable_ext) ≡ word16.
+unification hint 0 ≔ ⊢ carr word16_is_comparable ≡ comp_num (comp_num exadecim).
+unification hint 0 ≔ ⊢ carr word16_is_comparable ≡ comp_num byte8.
+unification hint 0 ≔ ⊢ carr word16_is_comparable ≡ word16.
(* operatore estensione unsigned *)
ndefinition extu_w16 ≝ λb2.〈zeroc ?:b2〉.