source: src/LIN/LIN.ma @ 878

Last change on this file since 878 was 878, checked in by campbell, 9 years ago

Removal of manually inserted record projections.

File size: 869 bytes
RevLine 
[723]1include "LIN/JointLTLLIN.ma".
2 
[757]3definition pre_lin_statement ≝ joint_statement unit.
[491]4
[757]5definition lin_statement ≝
[722]6  λglobals.
[757]7    option ident × (pre_lin_statement globals).
[491]8
[757]9definition well_formed_P ≝
[723]10  λA, B: Type[0].
11  λcode: list (option A × B).
12    match code with
13    [ nil ⇒ False
14    | cons hd tl ⇒
15      match \fst hd with
16      [ Some lbl ⇒ False
17      | None ⇒ True
18      ]
19    ].
20   
[757]21inductive lin_function_definition (globals: list ident): Type[0] ≝
22  lin_fu_internal: ∀code: list (lin_statement globals). well_formed_P ? ? code → lin_function_definition globals
23| lin_fu_external: external_function → lin_function_definition globals.
[491]24
[757]25record lin_program: Type[0] ≝
[491]26{
[757]27  lin_pr_vars: list (ident × nat);
28  lin_pr_funcs: list (ident × (lin_function_definition (map ? ? (fst ? ?) lin_pr_vars)));
29  lin_pr_main: option ident
[699]30}.
Note: See TracBrowser for help on using the repository browser.