Changeset 2947


Ignore:
Timestamp:
Mar 24, 2013, 9:17:34 PM (4 years ago)
Author:
campbell
Message:

Init change in measurable to structured file.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/MeasurableToStructured.ma

    r2914 r2947  
    8282λp.
    8383  let ge ≝ make_global p in
    84   do m ← init_mem … (λx.[Init_space x]) p;
     84  do m ← init_mem … (λx.x) p;
    8585  let main ≝ prog_main ?? p in
    8686  do b as Eb ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);
Note: See TracChangeset for help on using the changeset viewer.