Changeset 1132
- Timestamp:
- Aug 29, 2011, 5:30:25 PM (10 years ago)
- Location:
- src
- Files:
-
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LIN/JointLTLLIN.ma
r1110 r1132 27 27 inductive joint_statement (A: Type[0]) (globals: list ident): Type[0] ≝ 28 28 | joint_st_sequential: joint_instruction globals → A → joint_statement A globals 29 | joint_st_goto: label → joint_statement A globals 29 30 | joint_st_return: joint_statement A globals. -
src/LIN/LIN.ma
r1110 r1132 1 1 include "LIN/JointLTLLIN.ma". 2 2 3 inductive pre_lin_statement (globals: list ident): Type[0] ≝ 4 | lin_st_lift : joint_statement unit globals → pre_lin_statement globals 5 | lin_st_goto: label → pre_lin_statement globals. 3 definition pre_lin_statement ≝ joint_statement unit. 6 4 7 5 definition lin_statement ≝ -
src/LTL/LTL.ma
r1110 r1132 3 3 include "LIN/LIN.ma". 4 4 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. 5 definition ltl_statement ≝ joint_statement label. 8 6 9 7 definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
Note: See TracChangeset
for help on using the changeset viewer.