Changeset 753 for src/LTL/LTL.ma


Ignore:
Timestamp:
Apr 14, 2011, 5:54:37 PM (9 years ago)
Author:
mulligan
Message:

Work from today.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTL.ma

    r723 r753  
    2121  | LTL_Fu_ExternalFunction: ExternalFunction → LTLFunctionDefinition globals.
    2222 
    23 record LTLProgram (globals: list Identifier): Type[0] ≝
     23record LTLProgram (globals: list (Identifier × nat)): Type[0] ≝
    2424{
    25   LTL_Pr_Vars: list (Identifier × nat); (* 2nd component = size *)
    26   LTL_Pr_Funs: list (Identifier × (LTLFunctionDefinition globals));
     25  LTL_Pr_Funs: list (Identifier × (LTLFunctionDefinition (map ? ? \fst globals)));
    2726  LTL_Pr_Main: option Identifier
    2827}.
Note: See TracChangeset for help on using the changeset viewer.