Changeset 2947
- Timestamp:
- Mar 24, 2013, 9:17:34 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/MeasurableToStructured.ma
r2914 r2947 82 82 λp. 83 83 let ge ≝ make_global p in 84 do m ← init_mem … (λx. [Init_space x]) p;84 do m ← init_mem … (λx.x) p; 85 85 let main ≝ prog_main ?? p in 86 86 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.