Changeset 1930 for src/common
 Timestamp:
 May 9, 2012, 6:30:41 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/IOMonad.ma
r1920 r1930 237 237  #m #f #v #P #H #E whd in E:(??%?); destruct 238 238 ] qed. 239 240 lemma bindIO_inversion: ∀O,I. 241 ∀A,B: Type[0]. ∀f: IO O I A. ∀g: A → IO O I B. ∀y: B. 242 (f »= g = return y) → 243 ∃x. (f = return x) ∧ (g x = return y). 244 #O #I #A #B #f #g #y cases f normalize 245 [ #o #k #E destruct 246  #a #e %{a} /2 by conj/ 247  #m #H destruct (H) 248 ] qed. 249 250 (* When something in the error monad has found its way into the IO monad, 251 ensure that we can implicitly go back. *) 252 lemma io_eq_to_res : ∀O,I. ∀T:Type[0]. ∀e:res T. ∀v. 253 err_to_io … e = Value O I T v → 254 e = OK T v. 255 #O #I #T * 256 [ #e #v #E normalize in E; destruct @refl 257  #m #v #E normalize in E; destruct 258 ] 259 qed. 260 261 coercion io_eq_from_res : 262 ∀O,I,T,e,v. ∀E:err_to_io O I T e = Value O I T v. e = OK T v ≝ io_eq_to_res 263 on _E:eq (IO ???) ?? to eq (res ?) ??. 264
Note: See TracChangeset
for help on using the changeset viewer.