Ignore:
Timestamp:
Apr 4, 2012, 6:48:26 PM (9 years ago)
Author:
campbell
Message:

Update Cexec soundness proof.
Change finishes_with predicate to inductive form so that qed no longer
spends huge amounts of time typechecking.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/duff.test.ma

    r1513 r1876  
    33example exec: finishes_with (repr I32 6) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
    44normalize  (* you can examine the result here *)
    5 @refl
     5%
    66qed.
Note: See TracChangeset for help on using the changeset viewer.