Changeset 878 for src/ERTL


Ignore:
Timestamp:
Jun 3, 2011, 5:35:27 PM (9 years ago)
Author:
campbell
Message:

Removal of manually inserted record projections.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r783 r878  
    4949}.
    5050
    51 definition ertl_if_params: ertl_internal_function → nat.
    52   # E
    53   cases E
    54   # H1 # H2 # H3 # H4 # H5 # H6 # H7 # H8
    55   @ H3
    56 qed.
    57 
    58 definition ertl_if_stacksize: ertl_internal_function → nat.
    59   # E
    60   cases E
    61   # H1 # H2 # H3 # H4 # H5 # H6 # H7 # H8
    62   @ H5
    63 qed.
    64 
    6551inductive ertl_function: Type[0] ≝
    6652  | ertl_f_internal: ertl_internal_function → ertl_function
     
    7359  ertl_pr_main: option ident
    7460}.
    75 
    76 definition ertl_pr_vars: ertl_program → list (ident × nat).
    77   # E
    78   cases E
    79   # H1 # H2 # H3
    80   @ H1
    81 qed.
Note: See TracChangeset for help on using the changeset viewer.