Changeset 1110 for src/LIN


Ignore:
Timestamp:
Aug 24, 2011, 6:45:01 PM (8 years ago)
Author:
mulligan
Message:

changes to get ltl to lin pass to work properly

Location:
src/LIN
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/JointLTLLIN.ma

    r1108 r1110  
    77
    88inductive joint_instruction (globals: list ident): Type[0] ≝
    9   | joint_instr_skip: joint_instruction globals
    109  | joint_instr_comment: String → joint_instruction globals
    1110  | joint_instr_cost_label: costlabel → joint_instruction globals
  • src/LIN/LIN.ma

    r878 r1110  
    11include "LIN/JointLTLLIN.ma".
    22 
    3 definition pre_lin_statement ≝ joint_statement unit.
     3inductive pre_lin_statement (globals: list ident): Type[0] ≝
     4  | lin_st_lift : joint_statement unit globals → pre_lin_statement globals
     5  | lin_st_goto: label → pre_lin_statement globals.
    46
    57definition lin_statement ≝
Note: See TracChangeset for help on using the changeset viewer.