|
Last change
on this file since 2226 was
1601,
checked in by sacerdot, 9 years ago
|
|
Files ported to new version of the standard library.
|
|
File size:
734 bytes
|
| Line | |
|---|
| 1 | include "LIN/joint_LTL_LIN.ma". |
|---|
| 2 | include "basics/lists/list.ma". |
|---|
| 3 | |
|---|
| 4 | definition lin_params_ : params_ ≝ mk_params_ ltl_lin_params__ unit. |
|---|
| 5 | |
|---|
| 6 | definition pre_lin_statement ≝ joint_statement lin_params_. |
|---|
| 7 | definition lin_statement≝ λglobals.(option label) × (pre_lin_statement globals). |
|---|
| 8 | |
|---|
| 9 | definition lin_params: ∀globals. params globals ≝ |
|---|
| 10 | λglobals. |
|---|
| 11 | mk_params globals unit ltl_lin_params1 (list (lin_statement globals)) |
|---|
| 12 | (λcode. λl. |
|---|
| 13 | find ?? (λs. let 〈l',x〉 ≝ s in |
|---|
| 14 | match l' with [ None ⇒ None … | Some l'' ⇒ if eq_identifier … l l'' then Some … x else None ?]) code). |
|---|
| 15 | |
|---|
| 16 | definition lin_function ≝ λglobals. joint_function … (lin_params globals). |
|---|
| 17 | definition lin_program ≝ joint_program lin_params. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
