Changeset 1110 for src/LTL/LTL.ma


Ignore:
Timestamp:
Aug 24, 2011, 6:45:01 PM (10 years ago)
Author:
mulligan
Message:

changes to get ltl to lin pass to work properly

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/LTL/LTL.ma

    r1089 r1110  
    33include "LIN/LIN.ma".
    44
    5 definition ltl_statement ≝ joint_statement label.
     5inductive 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.
    68 
    79definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
Note: See TracChangeset for help on using the changeset viewer.