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