X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly2%2Fnum%2Fword16.ma;h=9d8c413c484d59e7024bc30d3b874ddd88072c50;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=c0d331a5af53a161de698bd93038760eb45d884b;hpb=bd112857523fc543c78cd29b74417585033ec464;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly2/num/word16.ma b/helm/software/matita/contribs/ng_assembly2/num/word16.ma
index c0d331a5a..9d8c413c4 100755
--- a/helm/software/matita/contribs/ng_assembly2/num/word16.ma
+++ b/helm/software/matita/contribs/ng_assembly2/num/word16.ma
@@ -34,10 +34,14 @@ ndefinition mk_word16 ≝ λb1,b2.mk_comp_num byte8 b1 b2.
 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〉.