include "LIN/JointLTLLIN.ma".
  
definition pre_lin_statement ≝ joint_statement unit.

definition lin_statement ≝
  λglobals.
    option ident × (pre_lin_statement globals).

definition well_formed_P ≝
  λA, B: Type[0].
  λcode: list (option A × B).
    match code with
    [ nil ⇒ False
    | cons hd tl ⇒
      match \fst hd with
      [ Some lbl ⇒ False
      | None ⇒ True
      ]
    ].
    
inductive lin_function_definition (globals: list ident): Type[0] ≝
  lin_fu_internal: ∀code: list (lin_statement globals). well_formed_P ? ? code → lin_function_definition globals
| lin_fu_external: external_function → lin_function_definition globals.

record lin_program: Type[0] ≝
{
  lin_pr_vars: list (ident × nat);
  lin_pr_funcs: list (ident × (lin_function_definition (map ? ? (fst ? ?) lin_pr_vars)));
  lin_pr_main: option ident
}.