freescale porting

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

diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
index b0c0faf197fe5a945194ebe0cca03414bafe5db1..e75c80bd653c71c53955c2e2c2ea20d375eff6bd 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma
@@ -15,8 +15,8 @@
 (* ********************************************************************** *)
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
-(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -1378,6 +1378,13 @@ ndefinition compl_ex ≝
  | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
  | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
 
+(* operatore x in [inf,sup] o in sup],[inf *)
+ndefinition inrange_ex ≝
+λx,inf,sup:exadecim.
+ match le_ex inf sup with
+  [ true ⇒ and_bool | false ⇒ or_bool ]
+ (le_ex inf x) (le_ex x sup).
+
 (* iteratore sugli esadecimali *)
 ndefinition forall_ex ≝ λP.
  P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗