source: src/LIN/LIN.ma @ 2131

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

Files ported to new version of the standard library.

File size: 734 bytes
RevLine 
[1378]1include "LIN/joint_LTL_LIN.ma".
[1601]2include "basics/lists/list.ma".
[491]3
[1378]4definition lin_params_ : params_ ≝ mk_params_ ltl_lin_params__ unit.
[1168]5
[1246]6definition pre_lin_statement ≝ joint_statement lin_params_.
[1379]7definition lin_statement≝ λglobals.(option label) × (pre_lin_statement globals).
[1168]8
[1246]9definition lin_params: ∀globals. params globals ≝
[1224]10 λglobals.
[1379]11  mk_params globals unit ltl_lin_params1 (list (lin_statement globals))
12   (λcode. λl.
[1246]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).
[1224]15
[1264]16definition lin_function ≝ λglobals. joint_function … (lin_params globals).
[1379]17definition lin_program ≝ joint_program lin_params.
Note: See TracBrowser for help on using the repository browser.