|
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
|
| Line | |
|---|
| 1 | include "joint/Joint.ma". |
|---|
| 2 | |
|---|
| 3 | definition ltl_params_: params_ ≝ |
|---|
| 4 | mk_params_ (mk_params__ unit unit unit unit registers_move Register nat unit False unit unit unit) label. |
|---|
| 5 | |
|---|
| 6 | definition ltl_statement ≝ joint_statement ltl_params_. |
|---|
| 7 | |
|---|
| 8 | definition ltl_params: ∀globals. params globals ≝ graph_params ltl_params_. |
|---|
| 9 | |
|---|
| 10 | definition ltl_program ≝ joint_program ltl_params. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
