Elimination principles are now processed in O(1) again

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / memory_struct.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma
index d256fefd85f57b8e2f4c7b70a8a2df4c7af6afde..0ba7735af38d1e1ed690cc7ef87d6f3d1d198af1 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma
@@ -33,7 +33,7 @@ ninductive memory_type : Type ≝
 | MEM_READ_WRITE: memory_type
 | MEM_OUT_OF_BOUND: memory_type.
 
-ndefinition memory_type_ind : ΠP:memory_type → Prop.P MEM_READ_ONLY → P MEM_READ_WRITE → P MEM_OUT_OF_BOUND → Πm:memory_type.P m ≝
+(*ndefinition memory_type_ind : ΠP:memory_type → Prop.P MEM_READ_ONLY → P MEM_READ_WRITE → P MEM_OUT_OF_BOUND → Πm:memory_type.P m ≝
 λP:memory_type → Prop.λp:P MEM_READ_ONLY.λp1:P MEM_READ_WRITE.λp2:P MEM_OUT_OF_BOUND.λm:memory_type.
  match m with [ MEM_READ_ONLY ⇒ p | MEM_READ_WRITE ⇒ p1 | MEM_OUT_OF_BOUND ⇒ p2 ].
 
@@ -44,7 +44,7 @@ ndefinition memory_type_rec : ΠP:memory_type → Set.P MEM_READ_ONLY → P MEM_
 ndefinition memory_type_rect : ΠP:memory_type → Type.P MEM_READ_ONLY → P MEM_READ_WRITE → P MEM_OUT_OF_BOUND → Πm:memory_type.P m ≝
 λP:memory_type → Type.λp:P MEM_READ_ONLY.λp1:P MEM_READ_WRITE.λp2:P MEM_OUT_OF_BOUND.λm:memory_type.
  match m with [ MEM_READ_ONLY ⇒ p | MEM_READ_WRITE ⇒ p1 | MEM_OUT_OF_BOUND ⇒ p2 ].
-
+*)
 (* **************** *)
 (* TIPO ARRAY DA 16 *)
 (* **************** *)
@@ -55,7 +55,7 @@ array_16T : T → T → T → T → T → T → T → T →
             T → T → T → T → T → T → T → T →
             Array16T T.
 
-ndefinition Array16T_ind
+(*ndefinition Array16T_ind
  : ΠT:Type.ΠP:Array16T T → Prop.
    (Πt,t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15.P (array_16T T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15)) → Πa:Array16T T.P a ≝
 λT:Type.λP:Array16T T → Prop.
@@ -75,7 +75,7 @@ ndefinition Array16T_rect
 λT:Type.λP:Array16T T → Type.
 λf:Πt,t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15.P (array_16T T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15).λa:Array16T T.
  match a with [ array_16T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 ⇒ f t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 ].
-
+*)
 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
 (* posso definire un getter a matrice sull'array *)
 ndefinition getn_array16T ≝
@@ -337,7 +337,7 @@ ninductive Array8T (T:Type) : Type ≝
 array_8T : T → T → T → T → T → T → T → T →
            Array8T T.
 
-ndefinition Array8T_ind
+(*ndefinition Array8T_ind
  : ΠT:Type.ΠP:Array8T T → Prop.
    (Πt,t1,t2,t3,t4,t5,t6,t7.P (array_8T T t t1 t2 t3 t4 t5 t6 t7)) → Πa:Array8T T.P a ≝
 λT:Type.λP:Array8T T → Prop.
@@ -357,7 +357,7 @@ ndefinition Array8T_rect
 λT:Type.λP:Array8T T → Type.
 λf:Πt,t1,t2,t3,t4,t5,t6,t7.P (array_8T T t t1 t2 t3 t4 t5 t6 t7).λa:Array8T T.
  match a with [ array_8T t t1 t2 t3 t4 t5 t6 t7 ⇒ f t t1 t2 t3 t4 t5 t6 t7 ].
-
+*)
 (* abbiamo gia' gli ottali come tipo induttivo quindi: *)
 (* posso definire un getter a matrice sull'array *)
 ndefinition getn_array8T ≝