freescale porting

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

diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8.ma b/helm/software/matita/contribs/ng_assembly/num/byte8.ma
index e899a698977b2215c9968956ae1a92e32fc178b0..d759181cebea9ffeb1ee66b290d7bb5014966c98 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/byte8.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/byte8.ma
@@ -306,9 +306,12 @@ ndefinition daa_b8 ≝
    pair … X'' true
   ].
 
-(* operatore x in [inf,sup] *)
+(* operatore x in [inf,sup] o in sup],[inf *)
 ndefinition inrange_b8 ≝
-λx,inf,sup:byte8.(le_b8 inf x) ⊗ (le_b8 x sup).
+λx,inf,sup:byte8.
+ match le_b8 inf sup with
+  [ true ⇒ and_bool | false ⇒ or_bool ]
+ (le_b8 inf x) (le_b8 x sup).
 
 (* iteratore sui byte *)
 ndefinition forall_b8 ≝