Changeset 756 for src/RTL


Ignore:
Timestamp:
Apr 15, 2011, 5:47:32 PM (9 years ago)
Author:
mulligan
Message:

Made a start on RTL. Renaming in ERTL and below to move closer to Brian's naming convention and datatypes.

Location:
src/RTL
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL.ma

    r754 r756  
    4444}.
    4545
     46definition rtl_if_stacksize: rtl_internal_function → nat.
     47  # R
     48  cases R
     49  # H1 # H2 # H3 # H4 # H5 # H6 # H7 # H8 # H9 # H10
     50  @ H7
     51qed.
     52
    4653inductive rtl_function_definition: Type[0] ≝
    4754  | rtl_f_internal: rtl_internal_function → rtl_function_definition
     
    5461  rtl_pr_main: option ident
    5562}.
    56 }.
Note: See TracChangeset for help on using the changeset viewer.