Changeset 2562 for src/joint/Joint.ma


Ignore:
Timestamp:
Dec 19, 2012, 10:38:43 AM (7 years ago)
Author:
piccolo
Message:

linearise modified

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2561 r2562  
    136136
    137137inductive joint_step (p : unserialized_params) (globals : list ident) : Type[0] ≝
    138   | step_seq : joint_seq p globals → joint_step p globals
    139138  | CALL: (ident + (dpl_arg p × (dph_arg p))) → call_args p → call_dest p → joint_step p globals
    140   | COND: acc_a_reg p → label → joint_step p globals.
     139  | COND: acc_a_reg p → label → joint_step p globals
     140  | step_seq : joint_seq p globals → joint_step p globals.
    141141
    142142coercion seq_to_step : ∀p,globals.∀s : joint_seq p globals.joint_step p globals ≝
Note: See TracChangeset for help on using the changeset viewer.