-ndefinition tick_result_ind
- : ΠA:Type.ΠP:tick_result A → Prop.(Πa:A.Πn:error_type.P (TickERR A a n)) →
- (Πa:A.Πn:susp_type.P (TickSUSP A a n)) → (Πa:A.P (TickOK A a))→Πt:tick_result A.P t ≝
-λA:Type.λP:tick_result A → Prop.λf:Πa:A.Πn:error_type.P (TickERR A a n).
-λf1:Πa:A.Πn:susp_type.P (TickSUSP A a n).λf2:Πa:A.P (TickOK A a).λt:tick_result A.
- match t with [ TickERR a n ⇒ f a n | TickSUSP a n ⇒ f1 a n | TickOK a ⇒ f2 a ].
-
-ndefinition tick_result_rec
- : ΠA:Type.ΠP:tick_result A → Set.(Πa:A.Πn:error_type.P (TickERR A a n)) →
- (Πa:A.Πn:susp_type.P (TickSUSP A a n)) → (Πa:A.P (TickOK A a))→Πt:tick_result A.P t ≝
-λA:Type.λP:tick_result A → Set.λf:Πa:A.Πn:error_type.P (TickERR A a n).
-λf1:Πa:A.Πn:susp_type.P (TickSUSP A a n).λf2:Πa:A.P (TickOK A a).λt:tick_result A.
- match t with [ TickERR a n ⇒ f a n | TickSUSP a n ⇒ f1 a n | TickOK a ⇒ f2 a ].
-
-ndefinition tick_result_rect
- : ΠA:Type.ΠP:tick_result A → Type.(Πa:A.Πn:error_type.P (TickERR A a n)) →
- (Πa:A.Πn:susp_type.P (TickSUSP A a n)) → (Πa:A.P (TickOK A a))→Πt:tick_result A.P t ≝
-λA:Type.λP:tick_result A → Type.λf:Πa:A.Πn:error_type.P (TickERR A a n).
-λf1:Πa:A.Πn:susp_type.P (TickSUSP A a n).λf2:Πa:A.P (TickOK A a).λt:tick_result A.
- match t with [ TickERR a n ⇒ f a n | TickSUSP a n ⇒ f1 a n | TickOK a ⇒ f2 a ].
-