-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 ].
-