Changeset 2044 for src/common/IOMonad.ma


Ignore:
Timestamp:
Jun 12, 2012, 10:52:37 AM (8 years ago)
Author:
campbell
Message:

PCs for RTLabs structured traces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/IOMonad.ma

    r1976 r2044  
    367367
    368368(* Inversion when injecting errors into IO monad. *)
    369 lemma bind_res_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop.
     369lemma bind_res_value : ∀O,I,A,B,e,f,v. ∀P:B → Type[0].
    370370  (∀a. e = OK A a → f a = OK B v → P v) →
    371371  (match e »= f with [ OK v ⇒ Value … v | Error m ⇒ Wrong … m ] = Value O I B v → P v).
     
    376376] qed.
    377377
    378 lemma bindIO_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop.
     378lemma bindIO_value : ∀O,I,A,B,e,f,v. ∀P:B → Type[0].
    379379  (∀a. e = Value ??? a → f a = Value ??? v → P v) →
    380380  (bindIO O I A B e f = Value ??? v → P v).
Note: See TracChangeset for help on using the changeset viewer.