source: src/LIN/joint_LTL_LIN.ma @ 1451

Last change on this file since 1451 was 1378, checked in by sacerdot, 8 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 
1include "joint/Joint.ma".
2
3inductive registers_move: Type[0] ≝
4 | from_acc: Register → registers_move
5 | to_acc: Register → registers_move.
6
7definition ltl_lin_params__: params__ ≝
8 mk_params__ unit unit unit unit registers_move Register nat unit False.
9definition ltl_lin_params0 : params0 ≝ mk_params0 ltl_lin_params__ unit unit.
10definition ltl_lin_params1 : params1 ≝ mk_params1 ltl_lin_params0 unit.
Note: See TracBrowser for help on using the repository browser.