Changeset 1239 for src/RTL


Ignore:
Timestamp:
Sep 21, 2011, 5:21:39 PM (9 years ago)
Author:
sacerdot
Message:

RTLAbstoRTL ported to new datatypes.

Note: RTL syntax/semantics is not (yet?) an instance of Joint.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL.ma

    r1115 r1239  
    5151
    5252definition rtl_function_definition ≝ fundef rtl_internal_function.
    53  
    54 record rtl_program: Type[0] ≝
    55 {
    56   rtl_pr_vars: list (ident × nat);
    57   rtl_pr_functs: list (ident × rtl_function_definition);
    58   rtl_pr_main: option ident
    59 }.
     53
     54definition rtl_program: Type[0] ≝ program (λ_.rtl_function_definition) nat.
Note: See TracChangeset for help on using the changeset viewer.