Changeset 3562 for LTS/stack.ma


Ignore:
Timestamp:
Jun 16, 2015, 3:19:27 PM (4 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/stack.ma

    r3560 r3562  
    8282
    8383definition stack_state_params:state_params≝
    84 mk_state_params stack_instr_params imp_env_params flat_labels frame_store_t (*DeqEnv*).
     84mk_state_params stack_instr_params frame_env_params flat_labels frame_store_t (*DeqEnv*).
    8585
    8686definition push : (store_type stack_state_params) → DeqNat → option (store_type stack_state_params) ≝
     
    131131  [ mk_signature fun fpt rt ⇒
    132132    !〈n,st1〉 ← pop st;
    133     frame_assign_var 〈(〈(nil ?),var〉::(\fst st1)),(\snd st1)〉 fpt n
     133    frame_assign_var 〈(〈(nil ?),var〉::(\fst st1)),(\snd st1)〉 O n
    134134  ].
    135135
     
    154154
    155155
    156 definition stack_envitem≝ (env_item imp_env_params stack_instr_params flat_labels).
     156definition stack_envitem≝ (env_item frame_env_params stack_instr_params flat_labels).
Note: See TracChangeset for help on using the changeset viewer.