Changeset 1168 for src/LTL


Ignore:
Timestamp:
Sep 2, 2011, 11:36:15 AM (8 years ago)
Author:
sacerdot
Message:

Joint statements parameterized over a record.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTL.ma

    r1166 r1168  
    11include "common/Graphs.ma".
    22include "utilities/IdentifierTools.ma".
    3 include "LIN/JointLTLLIN.ma".
     3include "joint/Joint.ma".
    44
    5 inductive ltl_statement (globals: list ident): Type[0] ≝
    6   ltl_st_lift_joint: joint_statement label Register Register Register Register Register registers_move globals → ltl_statement globals.
     5definition ltl_params: params ≝
     6 mk_params unit unit unit unit registers_move Register.
     7
     8definition ltl_statement ≝ λglobals: list ident. joint_statement label ltl_params globals.
    79 
    810definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
Note: See TracChangeset for help on using the changeset viewer.