Changeset 1070 for src/RTLabs/syntax.ma


Ignore:
Timestamp:
Jul 15, 2011, 12:56:48 PM (10 years ago)
Author:
campbell
Message:

Show that entry and exit labels are in the RTLabs graph.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/RTLabs/syntax.ma

    r1056 r1070  
    3535; f_stacksize : nat
    3636; f_graph     : graph statement
    37 ; f_entry     : label
    38 ; f_exit      : label
     37; f_entry     : Σl:label. ∃s. lookup ?? f_graph l = Some ? s
     38; f_exit      : Σl:label. ∃s. lookup ?? f_graph l = Some ? s
    3939}.
    4040
Note: See TracChangeset for help on using the changeset viewer.