Changeset 2044 for src/common
 Timestamp:
 Jun 12, 2012, 10:52:37 AM (7 years ago)
 Location:
 src/common
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/common/IOMonad.ma
r1976 r2044 367 367 368 368 (* Inversion when injecting errors into IO monad. *) 369 lemma bind_res_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop.369 lemma bind_res_value : ∀O,I,A,B,e,f,v. ∀P:B → Type[0]. 370 370 (∀a. e = OK A a → f a = OK B v → P v) → 371 371 (match e »= f with [ OK v ⇒ Value … v  Error m ⇒ Wrong … m ] = Value O I B v → P v). … … 376 376 ] qed. 377 377 378 lemma bindIO_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop.378 lemma bindIO_value : ∀O,I,A,B,e,f,v. ∀P:B → Type[0]. 379 379 (∀a. e = Value ??? a → f a = Value ??? v → P v) → 380 380 (bindIO O I A B e f = Value ??? v → P v). 
src/common/StructuredTraces.ma
r1976 r2044 250 250 (* Version in Prop for showing existence. *) 251 251 coinductive trace_label_diverges_exists (S:abstract_status) : S → Prop ≝ 252  tld_step :252  tld_step': 253 253 ∀status_initial: S. 254 254 ∀status_labelled: S. … … 256 256 trace_label_diverges_exists S status_labelled → 257 257 trace_label_diverges_exists S status_initial 258  tld_base :258  tld_base': 259 259 ∀status_initial: S. 260 260 ∀status_pre_fun_call: S.
Note: See TracChangeset
for help on using the changeset viewer.