Changeset 764 for src/RTLabs/syntax.ma


Ignore:
Timestamp:
Apr 20, 2011, 5:38:58 PM (9 years ago)
Author:
campbell
Message:

Start Cminor to RTLabs phase.

Includes some syntax for matching triples for convenience.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/RTLabs/syntax.ma

    r762 r764  
    7474λf.match f with [ mk_internal_function _ _ _ _ _ _ _ s _ _  _ ⇒ s ].
    7575
    76 (* Global variables only need to be given their size at this stage of
    77    compilation. *)
     76(* Note that the global variables will be initialised by the code in main
     77   by this stage.  All initialisation data should only reserve space. *)
    7878
    79 definition RTLabs_program ≝ program (fundef internal_function) nat.
     79definition RTLabs_program ≝ program (fundef internal_function) unit.
    8080
    8181(* TO CONSIDER:
Note: See TracChangeset for help on using the changeset viewer.