Changeset 2044 for src/common/IOMonad.ma
 Timestamp:
 Jun 12, 2012, 10:52:37 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/IOMonad.ma
r1976 r2044 367 367 368 368 (* Inversion when injecting errors into IO monad. *) 369 lemma bind_res_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop.369 lemma bind_res_value : ∀O,I,A,B,e,f,v. ∀P:B → Type[0]. 370 370 (∀a. e = OK A a → f a = OK B v → P v) → 371 371 (match e »= f with [ OK v ⇒ Value … v  Error m ⇒ Wrong … m ] = Value O I B v → P v). … … 376 376 ] qed. 377 377 378 lemma bindIO_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop.378 lemma bindIO_value : ∀O,I,A,B,e,f,v. ∀P:B → Type[0]. 379 379 (∀a. e = Value ??? a → f a = Value ??? v → P v) → 380 380 (bindIO O I A B e f = Value ??? v → P v).
Note: See TracChangeset
for help on using the changeset viewer.