X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly2%2Fnum%2Fword32.ma;h=7cc9461b252c7f4aa089375da8972dcadd6fa132;hb=647b419e96770d90a82d7a9e5e8843566a9f93ee;hp=4fbbe96fcb9a45e026a97f333a2322be37f7dcdd;hpb=bd112857523fc543c78cd29b74417585033ec464;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly2/num/word32.ma b/helm/software/matita/contribs/ng_assembly2/num/word32.ma
index 4fbbe96fc..7cc9461b2 100755
--- a/helm/software/matita/contribs/ng_assembly2/num/word32.ma
+++ b/helm/software/matita/contribs/ng_assembly2/num/word32.ma
@@ -33,11 +33,16 @@ ndefinition mk_word32 ≝ λw1,w2.mk_comp_num word16 w1 w2.
 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〉.