source: src/LIN/LIN.ma @ 1601

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

Files ported to new version of the standard library.

File size: 734 bytes
Line 
1include "LIN/joint_LTL_LIN.ma".
2include "basics/lists/list.ma".
3
4definition lin_params_ : params_ ≝ mk_params_ ltl_lin_params__ unit.
5
6definition pre_lin_statement ≝ joint_statement lin_params_.
7definition lin_statement≝ λglobals.(option label) × (pre_lin_statement globals).
8
9definition 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
16definition lin_function ≝ λglobals. joint_function … (lin_params globals).
17definition lin_program ≝ joint_program lin_params.
Note: See TracBrowser for help on using the repository browser.