|
Last change
on this file since 2217 was
1378,
checked in by sacerdot, 10 years ago
|
|
New file LIN/joint_LTL_LIN.ma to factorize out the syntactic parameters shared
by LTL and LIN.
|
|
File size:
416 bytes
|
| Line | |
|---|
| 1 | include "joint/Joint.ma". |
|---|
| 2 | |
|---|
| 3 | inductive registers_move: Type[0] ≝ |
|---|
| 4 | | from_acc: Register → registers_move |
|---|
| 5 | | to_acc: Register → registers_move. |
|---|
| 6 | |
|---|
| 7 | definition ltl_lin_params__: params__ ≝ |
|---|
| 8 | mk_params__ unit unit unit unit registers_move Register nat unit False. |
|---|
| 9 | definition ltl_lin_params0 : params0 ≝ mk_params0 ltl_lin_params__ unit unit. |
|---|
| 10 | definition ltl_lin_params1 : params1 ≝ mk_params1 ltl_lin_params0 unit. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
