source: src/Cminor/test/search.test.ma @ 1226

Last change on this file since 1226 was 1226, checked in by campbell, 8 years ago

Adjust pretty printers for change in program records, try a test of each.

File size: 451 bytes
Line 
1include "Cminor/test/search.Cminor.ma".
2
3
4   example exec: finishes_with (repr 3) ? (exec_up_to Cminor_fullexec myprog 1000 [ ]).
5   normalize  (* you can examine the result here *)
6   @refl qed.
7
8
9include "Cminor/toRTLabs.ma".
10include "RTLabs/semantics.ma".
11
12example execRTL: finishes_with (repr 3) ? (do myprog' ← cminor_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [ ]).
13normalize  (* you can examine the result here *)
14@refl
15qed.
16
17
Note: See TracBrowser for help on using the repository browser.