Changeset 1157 for src/Clight/test/factorial.c.ma

Timestamp:

Aug 31, 2011, 12:15:39 PM (10 years ago)

Author:

campbell

Message:

Update pretty printers and examples.

File:

• src/Clight/test/factorial.c.ma (modified) (2 diffs)

src/Clight/test/factorial.c.ma

@@ -2 +2 @@
 include "common/Animation.ma".
 
-definition myprog := mk_program clight_fundef type
+definition myprog := mk_program clight_fundef ((list init_data) × type)
   [〈ident_of_nat 0 (* get_input *), CL_External (ident_of_nat 0) Tnil (Tint I32 Signed  )〉;
   〈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)]).
 normalize  (* you can examine the result here *)
-@refl qed.
+@refl
+qed.