Changeset 1601 for src/common/IOMonad.ma


Ignore:
Timestamp:
Dec 13, 2011, 2:49:52 PM (8 years ago)
Author:
sacerdot
Message:

Files ported to new version of the standard library.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/IOMonad.ma

    r1599 r1601  
    6666(match a return λa'.P_io O I A P a' → ? with
    6767 [ Wrong m ⇒ λ_. Wrong O I ? m
    68  | Value c ⇒ λp'. Value ??? (dp A P c p')
     68 | Value c ⇒ λp'. Value ??? (mk_Sig A P c p')
    6969 | Interact out k ⇒ λp'. Interact ??? out (λv. io_inject_0 O I A P (k v) (p' v))
    7070 ]) p.
     
    8181match a with
    8282[ Wrong m ⇒ Wrong ??? m
    83 | Value b ⇒ match b with [ dp w p ⇒ Value ??? w]
     83| Value b ⇒ match b with [ mk_Sig w p ⇒ Value ??? w]
    8484| Interact out k ⇒ Interact ??? out (λv. io_eject ?? A P (k v))
    8585].
     
    9595
    9696lemma sig_bindIO_OK: ∀O,I,A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:IO O I (Sig A P). ∀f:Sig A P → IO O I B.
    97   (∀v:A. ∀p:P v. P_io O I ? P' (f (dp A P v p))) →
     97  (∀v:A. ∀p:P v. P_io O I ? P' (f (mk_Sig A P v p))) →
    9898  P_io O I ? P' (bindIO O I (Sig A P) B e f).
    9999#O #I #A #B #P #P' #e #f elim e;
Note: See TracChangeset for help on using the changeset viewer.