Changeset 125 for C-semantics/IOMonad.ma


Ignore:
Timestamp:
Sep 24, 2010, 10:31:32 AM (9 years ago)
Author:
campbell
Message:

Unify memory space / pointer types.
Implement global variable initialisation and lookup.
Global variables get memory spaces, local variables could be anywhere (for now).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/IOMonad.ma

    r25 r125  
    118118nqed.
    119119
     120nlemma opt_bindIO2_OK: ∀I,O,A,B,C. ∀P:C → Prop. ∀e:option (A×B). ∀f: A → B → IO I O C.
     121  (∀vA:A.∀vB:B. e = Some (A×B) 〈vA,vB〉 → P_io I O ? P (f vA vB)) →
     122  P_io I O ? P (bindIO2 I O A B C e f).
     123#I O A B C P e; nelim e; //; #v; ncases v; #vA vB f H; napply H; //;
     124nqed.
     125
    120126nlemma bindIO_OK: ∀I,O,A,B. ∀P:B → Prop. ∀e:IO I O A. ∀f: A → IO I O B.
    121127  (∀v:A. P_io I O ? P (f v)) →
Note: See TracChangeset for help on using the changeset viewer.