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