Ignore:
Timestamp:
Sep 16, 2011, 7:16:44 PM (8 years ago)
Author:
campbell
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/test/search.Cminor.ma

    r1157 r1226  
    281281
    282282definition myprog : Cminor_program :=
    283 mk_program ?? [
     283mk_program ?? [] [
    284284  (pair ?? id__div32u f__div32u);
    285285  (pair ?? id__div32s f__div32s);
     
    287287  (pair ?? id_main f_main)
    288288]  id_main
    289 []
    290289.
    291 
    292    example exec: finishes_with (repr 3) ? (exec_up_to Cminor_fullexec myprog 1000 [ ]).
    293    normalize  (* you can examine the result here *)
    294    @refl qed.
    295 
    296 
    297 include "Cminor/toRTLabs.ma".
    298 include "RTLabs/semantics.ma".
    299 
    300 example execRTL: finishes_with (repr 3) ? (do myprog' ← cminor_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [ ]).
    301 normalize  (* you can examine the result here *)
    302 @refl
    303 qed.
    304 
    305 
Note: See TracChangeset for help on using the changeset viewer.