source: src/LTL/LTL.ma @ 1270

Last change on this file since 1270 was 1270, checked in by sacerdot, 8 years ago

Making RTL syntax an instance of Joint.

File size: 364 bytes
RevLine 
[1222]1include "joint/Joint.ma".
[722]2
[1246]3definition ltl_params_: params_ ≝
[1270]4 mk_params_ (mk_params__ unit unit unit unit registers_move Register nat unit False unit unit unit) label.
[1168]5
[1246]6definition ltl_statement ≝ joint_statement ltl_params_.
[1222]7
[1252]8definition ltl_params: ∀globals. params globals ≝ graph_params ltl_params_.
[1222]9
[1233]10definition ltl_program ≝ joint_program ltl_params.
Note: See TracBrowser for help on using the repository browser.