Changeset 2500 for src/common/Errors.ma
 Timestamp:
 Nov 28, 2012, 5:57:38 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Errors.ma
r2496 r2500 273 273 ∀A,B,C: Type[0]. ∀f: res (A×B). ∀g: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C. ∀z. 274 274 bind2_eq ??? f g = return z → 275 ∃x. ∃y. ∃Eq. f = return 〈x, y〉 ∧g x y Eq = return z.275 ∃x. ∃y. ∃Eq. g x y Eq = return z. 276 276 #A #B #C #f cases f 277 [ * #a #b #g normalize #z #Heq %{a} %{b} %{(refl ? ?)} @conj try @refl@Heq277 [ * #a #b #g normalize #z #Heq %{a} %{b} %{(refl ? (OK ? 〈a,b〉))} @Heq 278 278  #errmsg #g #z normalize #Habsurd destruct (Habsurd) ] 279 qed. 279 qed. 280 280 281 281 definition res_to_opt : ∀A:Type[0]. res A → option A ≝
Note: See TracChangeset
for help on using the changeset viewer.