Changeset 2888


Ignore:
Timestamp:
Mar 15, 2013, 7:31:39 PM (4 years ago)
Author:
tranquil
Message:

backtracked some partial changes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTL.ma

    r2887 r2888  
    2323  the offset does not need the stack size to be computed *)
    2424
    25 check ltl_lin_seq
    2625definition preserve_carry_bit :
    27  (λglobals:list ident
    28   .λdo_it:bool
    29    .λsteps:step_block LTL globals
    30     .if do_it 
    31      then 〈[λ_:code_point LTL.SAVE_CARRY]@ \fst  (\fst  steps),
    32               \snd  (\fst  steps),
    33               \snd  steps@[RESTORE_CARRY]〉 
    34      else steps ).
    35 
    36 
    37   ∀globals.bool → step_block LTL globals → step_block LTL globals ≝
     26  ∀globals.bool → list (joint_seq LTL globals) → list (joint_seq LTL globals) ≝
    3827  λglobals,do_it,steps.
    39   if do_it then
    40     〈[?] @ (\fst(\fst steps)),
    41      \snd(\fst steps),
    42       (\snd  steps) @ [RESTORE_CARRY]〉
    43   else steps.
    44 #_ @SAVE_CARRY
    45 qed.
    46 check preserve_carry_bit
     28  if do_it then SAVE_CARRY :: steps @ [RESTORE_CARRY] else steps.
    4729
    4830(* for notation *)
Note: See TracChangeset for help on using the changeset viewer.