Changeset 1132 for src/LTL/LTL.ma


Ignore:
Timestamp:
Aug 29, 2011, 5:30:25 PM (8 years ago)
Author:
mulligan
Message:

reunified ltl and lin instruction type, removing lifting in ltl and lin and simplifying the ertl > ertl passes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTL.ma

    r1110 r1132  
    33include "LIN/LIN.ma".
    44
    5 inductive ltl_statement (globals: list ident): Type[0] ≝
    6   | ltl_st_lift: joint_statement label globals → ltl_statement globals
    7   | ltl_st_skip: label → ltl_statement globals.
     5definition ltl_statement ≝ joint_statement label.
    86 
    97definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
Note: See TracChangeset for help on using the changeset viewer.