Changeset 1876 for src/Clight/test/sum.test.ma
 Timestamp:
 Apr 4, 2012, 6:48:26 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/test/sum.test.ma
r1618 r1876 3 3 example exec: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec myprog 1000 [ ]). 4 4 normalize (* you can examine the result here *) 5 @refl 5 % 6 6 qed. 7 7 … … 10 10 example es: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [ ]). 11 11 normalize (* you can examine the result here *) 12 @refl 12 % 13 13 qed. 14 14 … … 20 20 (λp. exec_up_to Cminor_fullexec p 1000 [ ])). 21 21 normalize 22 @refl 22 % 23 23 qed. 24 24 … … 31 31 (λp2. exec_up_to RTLabs_fullexec p2 1000 [ ]))). 32 32 normalize 33 @refl 33 % 34 34 qed. 35 35 (*
Note: See TracChangeset
for help on using the changeset viewer.