Changeset 2145 for src/common/IOMonad.ma


Ignore:
Timestamp:
Jul 2, 2012, 4:12:12 PM (8 years ago)
Author:
campbell
Message:

Cost labelling doesn't affect interaction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/IOMonad.ma

    r2044 r2145  
    385385] qed.
    386386
     387lemma bindIO_res_interact : ∀O,I,A,B,e,f,o,k. ∀P:∀o:O. (I o → IO O I B) → Type[0].
     388  (∀v. e = OK A v → f v = Interact … o k → P o k) →
     389  bindIO O I A B (err_to_io … e) f = Interact … o k → P o k.
     390#O #I #A #B *
     391[ #a #f #o #k #P #H #E @(H … E) @refl
     392| #m #f #o #k #P #_ #E whd in E:(??%?); destruct
     393] qed.
     394
     395lemma bindIO_opt_interact : ∀O,I,A,B,m,e,f,o,k. ∀P:∀o:O. (I o → IO O I B) → Type[0].
     396  (∀v. e = Some A v → f v = Interact … o k → P o k) →
     397  bindIO O I A B (opt_to_io … m e) f = Interact … o k → P o k.
     398#O #I #A #B #m *
     399[ #f #o #k #P #_ #E whd in E:(??%?); destruct
     400| #a #f #o #k #P #H #E @(H … E) @refl
     401] qed.
     402
    387403lemma bindIO_inversion: ∀O,I.
    388404  ∀A,B: Type[0]. ∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
Note: See TracChangeset for help on using the changeset viewer.