freescale porting

[helm.git] / helm / software / matita / contribs / ng_assembly2 / num / word16.ma

diff --git a/helm/software/matita/contribs/ng_assembly2/num/word16.ma b/helm/software/matita/contribs/ng_assembly2/num/word16.ma
index c0d331a5af53a161de698bd93038760eb45d884b..9d8c413c484d59e7024bc30d3b874ddd88072c50 100755 (executable)
--- 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〉.