freescale porting, work in progress

[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 0ba7735af38d1e1ed690cc7ef87d6f3d1d198af1..38966a668791a002928c1fc24a2a8f5754aed7ba 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,18 +33,6 @@ 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 ≝
-λ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 ].
-
-ndefinition memory_type_rec : ΠP:memory_type → Set.P MEM_READ_ONLY → P MEM_READ_WRITE → P MEM_OUT_OF_BOUND → Πm:memory_type.P m ≝
-λP:memory_type → Set.λ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 ].
-
-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,27 +43,6 @@ array_16T : T → T → T → T → T → T → T → T →
             T → T → T → T → T → T → T → T →
             Array16T T.
 
-(*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.
-λ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 ].
-
-ndefinition Array16T_rec
- : ΠT:Type.ΠP:Array16T T → Set.
-   (Π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 → Set.
-λ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 ].
-
-ndefinition Array16T_rect
- : ΠT:Type.ΠP:Array16T T → Type.
-   (Π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 → 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,27 +304,6 @@ ninductive Array8T (T:Type) : Type ≝
 array_8T : T → T → T → T → T → T → T → T →
            Array8T T.
 
-(*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.
-λ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 ].
-
-ndefinition Array8T_rec
- : ΠT:Type.ΠP:Array8T T → Set.
-   (Π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 → Set.
-λ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 ].
-
-ndefinition Array8T_rect
- : ΠT:Type.ΠP:Array8T T → Type.
-   (Π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 → 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 ≝