Changeset 1603 for src/Clight/CexecComplete.ma
 Timestamp:
 Dec 13, 2011, 5:37:40 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/CexecComplete.ma
r1566 r1603 12 12 13 13 definition yields_sig : ∀A,P. res (Sig A P) → A → Prop ≝ 14 λA,P,e,v. match e with [ OK v' ⇒ match v' with [ dpv'' _ ⇒ v = v'' ]  _ ⇒ False].14 λA,P,e,v. match e with [ OK v' ⇒ match v' with [ mk_Sig v'' _ ⇒ v = v'' ]  _ ⇒ False]. 15 15 16 16 let rec yieldsIO_sig (A:Type[0]) (P:A → Prop) (e:IO io_out io_in (Sig A P)) (v:A) on e : Prop ≝ 17 17 match e with 18 [ Value v' ⇒ match v' with [ dpv'' _ ⇒ v = v'' ]18 [ Value v' ⇒ match v' with [ mk_Sig v'' _ ⇒ v = v'' ] 19 19  Interact _ k ⇒ ∃r.yieldsIO_sig A P (k r) v 20 20  _ ⇒ False]. … … 33 33 qed. 34 34 35 lemma yields_sig_eq: ∀A,P,e,v. yields_sig A P e v → ∃p. e = OK ? ( dp… v p).35 lemma yields_sig_eq: ∀A,P,e,v. yields_sig A P e v → ∃p. e = OK ? (mk_Sig … v p). 36 36 #A #P #e #v cases e; 37 37 [ #vp cases vp; #v' #p #H whd in H; >H %{ p} @refl
Note: See TracChangeset
for help on using the changeset viewer.