Changeset 2044 for src/common


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

PCs for RTLabs structured traces.

Location:
src/common
Files:
2 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).
  • src/common/StructuredTraces.ma

    r1976 r2044  
    250250(* Version in Prop for showing existence. *)
    251251coinductive trace_label_diverges_exists (S:abstract_status) : S → Prop ≝
    252   | tld_step:
     252  | tld_step':
    253253      ∀status_initial: S.
    254254      ∀status_labelled: S.
     
    256256          trace_label_diverges_exists S status_labelled →
    257257            trace_label_diverges_exists S status_initial
    258   | tld_base:
     258  | tld_base':
    259259      ∀status_initial: S.
    260260      ∀status_pre_fun_call: S.
Note: See TracChangeset for help on using the changeset viewer.