include "LIN/joint_LTL_LIN.ma".
include "basics/lists/list.ma".

definition lin_params_ : params_ ≝ mk_params_ ltl_lin_params__ unit.

definition pre_lin_statement ≝ joint_statement lin_params_.
definition lin_statement≝ λglobals.(option label) × (pre_lin_statement globals).

definition lin_params: ∀globals. params globals ≝
 λglobals.
  mk_params globals unit ltl_lin_params1 (list (lin_statement globals))
   (λcode. λl.
    find ?? (λs. let 〈l',x〉 ≝ s in
     match l' with [ None ⇒ None … | Some l'' ⇒ if eq_identifier … l l'' then Some … x else None ?]) code).

definition lin_function ≝ λglobals. joint_function … (lin_params globals).
definition lin_program ≝ joint_program lin_params.