Changeset 1157 for src/Clight/test/factorial.c.ma
- Timestamp:
- Aug 31, 2011, 12:15:39 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/test/factorial.c.ma
r978 r1157 2 2 include "common/Animation.ma". 3 3 4 definition myprog := mk_program clight_fundef type4 definition myprog := mk_program clight_fundef ((list init_data) × type) 5 5 [〈ident_of_nat 0 (* get_input *), CL_External (ident_of_nat 0) Tnil (Tint I32 Signed )〉; 6 6 〈ident_of_nat 1 (* main *), CL_Internal ( … … 41 41 example exec: finishes_with (repr I32 120) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]). 42 42 normalize (* you can examine the result here *) 43 @refl qed. 43 @refl 44 qed.
Note: See TracChangeset
for help on using the changeset viewer.