Changeset 1930 for src/common


Ignore:
Timestamp:
May 9, 2012, 6:30:41 PM (8 years ago)
Author:
campbell
Message:

Tidy up labelling simulation stuff a bit.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/IOMonad.ma

    r1920 r1930  
    237237| #m #f #v #P #H #E whd in E:(??%?); destruct
    238238] qed.
     239
     240lemma 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. *)
     252lemma 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]
     259qed.
     260
     261coercion 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.