Changeset 1222 for src/LTL/LTL.ma
- Timestamp:
- Sep 16, 2011, 11:02:23 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LTL/LTL.ma
r1183 r1222 1 include "joint/Joint.ma". 1 2 include "common/Graphs.ma". 2 include "utilities/IdentifierTools.ma".3 include "joint/Joint.ma".4 3 5 4 definition ltl_params: params ≝ … … 9 8 10 9 definition ltl_statement ≝ λglobals: list ident. joint_statement ltl_params globals. 11 12 definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals). 10 11 definition ltl_sem_params_: ∀globals. sem_params_ ltl_params globals ≝ 12 λglobals. 13 mk_sem_params_ ltl_params globals (graph (ltl_statement globals)) (lookup …). 14 15 definition ltl_program ≝ λglobals. joint_program globals … (ltl_sem_params_ globals). 16 (* 13 17 14 18 record ltl_internal_function (globals: list ident): Type[0] ≝ … … 31 35 ltl_pr_main: option ident 32 36 }. 37 *)
Note: See TracChangeset
for help on using the changeset viewer.