...

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma b/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma
index 83abb181625a358691467fb24c84df24a477ac84..5bfd406b5296052c5ca36c161a0f683706f6648a 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma
@@ -29,18 +29,6 @@ ninductive error_type : Type ≝
 | ILL_FETCH_AD: error_type
 | ILL_EX_AD: error_type.
 
-ndefinition error_type_ind : ΠP:error_type → Prop.P ILL_OP → P ILL_FETCH_AD → P ILL_EX_AD → Πe:error_type.P e ≝
-λP:error_type → Prop.λp:P ILL_OP.λp1:P ILL_FETCH_AD.λp2:P ILL_EX_AD.λe:error_type.
- match e with [ ILL_OP ⇒ p | ILL_FETCH_AD ⇒ p1 | ILL_EX_AD ⇒ p2 ].
-
-ndefinition error_type_rec : ΠP:error_type → Set.P ILL_OP → P ILL_FETCH_AD → P ILL_EX_AD → Πe:error_type.P e ≝
-λP:error_type → Set.λp:P ILL_OP.λp1:P ILL_FETCH_AD.λp2:P ILL_EX_AD.λe:error_type.
- match e with [ ILL_OP ⇒ p | ILL_FETCH_AD ⇒ p1 | ILL_EX_AD ⇒ p2 ].
-
-ndefinition error_type_rect : ΠP:error_type → Type.P ILL_OP → P ILL_FETCH_AD → P ILL_EX_AD → Πe:error_type.P e ≝
-λP:error_type → Type.λp:P ILL_OP.λp1:P ILL_FETCH_AD.λp2:P ILL_EX_AD.λe:error_type.
- match e with [ ILL_OP ⇒ p | ILL_FETCH_AD ⇒ p1 | ILL_EX_AD ⇒ p2 ].
-
 (* un tipo opzione ad hoc
    - errore: interessa solo l'errore
    - ok: interessa info e il nuovo pc
@@ -49,27 +37,6 @@ ninductive fetch_result (A:Type) : Type ≝
   FetchERR : error_type → fetch_result A
 | FetchOK  : A → word16 → fetch_result A.
 
-ndefinition fetch_result_ind
- : ΠA:Type.ΠP:fetch_result A → Prop.(Πn:error_type.P (FetchERR A n)) →
-   (Πa:A.Πn:word16.P (FetchOK A a n)) → Πf:fetch_result A.P f ≝
-λA:Type.λP:fetch_result A → Prop.λf:Πn:error_type.P (FetchERR A n).
-λf1:Πa:A.Πn:word16.P (FetchOK A a n).λf2:fetch_result A.
- match f2 with [ FetchERR n ⇒ f n | FetchOK a n ⇒ f1 a n ].
-
-ndefinition fetch_result_rec
- : ΠA:Type.ΠP:fetch_result A → Set.(Πn:error_type.P (FetchERR A n)) →
-   (Πa:A.Πn:word16.P (FetchOK A a n)) → Πf:fetch_result A.P f ≝
-λA:Type.λP:fetch_result A → Set.λf:Πn:error_type.P (FetchERR A n).
-λf1:Πa:A.Πn:word16.P (FetchOK A a n).λf2:fetch_result A.
- match f2 with [ FetchERR n ⇒ f n | FetchOK a n ⇒ f1 a n ].
-
-ndefinition fetch_result_rect
- : ΠA:Type.ΠP:fetch_result A → Type.(Πn:error_type.P (FetchERR A n)) →
-   (Πa:A.Πn:word16.P (FetchOK A a n)) → Πf:fetch_result A.P f ≝
-λA:Type.λP:fetch_result A → Type.λf:Πn:error_type.P (FetchERR A n).
-λf1:Πa:A.Πn:word16.P (FetchOK A a n).λf2:fetch_result A.
- match f2 with [ FetchERR n ⇒ f n | FetchOK a n ⇒ f1 a n ].
-
 (* **************************** *)
 (* FETCH E ACCESSO ALLA MEMORIA *)
 (* **************************** *)