Changeset 757 for src/LIN/LIN.ma
 Timestamp:
 Apr 18, 2011, 12:30:53 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/LIN/LIN.ma
r723 r757 1 1 include "LIN/JointLTLLIN.ma". 2 2 3 definition PreLINStatement ≝ JointStatement unit.3 definition pre_lin_statement ≝ joint_statement unit. 4 4 5 definition LINStatement ≝5 definition lin_statement ≝ 6 6 λglobals. 7 option Identifier × (PreLINStatement globals).7 option ident × (pre_lin_statement globals). 8 8 9 definition WellFormedP ≝9 definition well_formed_P ≝ 10 10 λA, B: Type[0]. 11 11 λcode: list (option A × B). … … 19 19 ]. 20 20 21 inductive LINFunctionDefinition (globals: list Identifier): Type[0] ≝22 LIN_Fu_Internal: ∀code: list (LINStatement globals). WellFormedP ? ? code → LINFunctionDefinition globals23  LIN_Fu_External: ExternalFunction → LINFunctionDefinition globals.21 inductive 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. 24 24 25 record LINProgram: Type[0] ≝25 record lin_program: Type[0] ≝ 26 26 { 27 LIN_Pr_vars: list (Identifier× nat);28 LIN_Pr_funs: list (Identifier × (LINFunctionDefinition (map ? ? (fst ? ?) LIN_Pr_vars)));29 LIN_Pr_main: option Identifier27 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 30 30 }. 31 31 32 definition LIN_Pr_vars:33 LINProgram → list (Identifier× nat).32 definition lin_pr_vars: 33 lin_program → list (ident × nat). 34 34 # r 35 35 cases r … … 38 38 qed. 39 39 40 definition LIN_Pr_funs:41 ∀p: LINProgram.42 list ( Identifier × (LINFunctionDefinition (map ? ? (fst ? ?) (LIN_Pr_vars p)))).40 definition lin_pr_funcs: 41 ∀p: lin_program. 42 list (ident × (lin_function_definition (map ? ? (fst ? ?) (lin_pr_vars p)))). 43 43 # r 44 44 cases r
Note: See TracChangeset
for help on using the changeset viewer.