Changeset 1071 for src/RTL/RTL.ma


Ignore:
Timestamp:
Jul 15, 2011, 2:40:40 PM (9 years ago)
Author:
mulligan
Message:

changes the specific form that the added proofs take to use None, not Some, hence removing the exitential

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL.ma

    r1068 r1071  
    3535  rtl_if_runiverse: universe RegisterTag;
    3636(*  rtl_if_sig: signature;  -- dropped in front end *)
    37   rtl_if_result: registers;
    38   rtl_if_params: registers;
    39   rtl_if_locals: registers;
     37  rtl_if_result   : registers;
     38  rtl_if_params   : registers;
     39  rtl_if_locals   : registers;
    4040  rtl_if_stacksize: nat;
    41   rtl_if_graph: rtl_statement_graph;
    42   rtl_if_entry: label;
    43   rtl_if_exit: label
     41  rtl_if_graph    : rtl_statement_graph;
     42  rtl_if_entry    : Σl: label. lookup ? ? rtl_if_graph l ≠ None ?;
     43  rtl_if_exit     : Σl: label. lookup ? ? rtl_if_graph l ≠ None ?
    4444}.
    4545
Note: See TracChangeset for help on using the changeset viewer.