Changeset 2688 for src/joint/Joint.ma


Ignore:
Timestamp:
Feb 21, 2013, 6:03:46 PM (8 years ago)
Author:
tranquil
Message:
  • in Arithmeticcs.ma: commented include that breaks script in latest matita
  • moved COST_LABEL out of joint_seq
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2681 r2688  
    9494inductive joint_seq (p:unserialized_params) (globals: list ident): Type[0] ≝
    9595  | COMMENT: String → joint_seq p globals
    96   | COST_LABEL: costlabel → joint_seq p globals
    9796  | MOVE: pair_move p → joint_seq p globals
    9897  | POP: acc_a_reg p → joint_seq p globals
     
    136135
    137136inductive joint_step (p : unserialized_params) (globals : list ident) : Type[0] ≝
     137  | COST_LABEL: costlabel → joint_step p globals
    138138  | CALL: (ident + (dpl_arg p × (dph_arg p))) → call_args p → call_dest p → joint_step p globals
    139139  | COND: acc_a_reg p → label → joint_step p globals
     
    152152    ]
    153153  | COND _ l ⇒ [l]
    154   | CALL _ _ _ ⇒ [ ]
     154  | _ ⇒ [ ]
    155155  ].
    156156
Note: See TracChangeset for help on using the changeset viewer.