Changeset 1380 for src/joint


Ignore:
Timestamp:
Oct 14, 2011, 10:25:03 PM (9 years ago)
Author:
sacerdot
Message:

LTL and LIN semantics factorized out in joint_LTL_LIN_semantics.ma.
Very cool.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r1282 r1380  
    172172definition joint_program ≝
    173173 λp:∀globals.params globals. program (λglobals. joint_function globals (p globals)) nat.
    174 
    175 (****************************************************************************)
    176 
    177 (* Used in LTL and LIN *) 
    178 inductive registers_move: Type[0] ≝
    179  | from_acc: Register → registers_move
    180  | to_acc: Register → registers_move.
Note: See TracChangeset for help on using the changeset viewer.