freescale porting

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

diff --git a/helm/software/matita/contribs/ng_assembly/num/word16.ma b/helm/software/matita/contribs/ng_assembly/num/word16.ma
index 2ae8fc5fd84352367bc04c11b6096a7dd06065dd..e89e64f3d81babb84715b4de1a9623f685c579c8 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/word16.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word16.ma
@@ -233,9 +233,12 @@ ndefinition div_b8 ≝
 (*    puo' essere sottratto al dividendo *) 
   | false ⇒ div_b8_aux w (rol_w16_n 〈〈x0,x0〉:b〉 nat7) 〈x8,x0〉 〈x0,x0〉 nat7 ]].
 
-(* operatore x in [inf,sup] *)
+(* operatore x in [inf,sup] o in sup],[inf *)
 ndefinition inrange_w16 ≝
-λx,inf,sup:word16.(le_w16 inf x) ⊗ (le_w16 x sup).
+λx,inf,sup:word16.
+ match le_w16 inf sup with
+  [ true ⇒ and_bool | false ⇒ or_bool ]
+ (le_w16 inf x) (le_w16 x sup).
 
 (* iteratore sulle word *)
 ndefinition forall_w16 ≝