Changeset 1371 for src/LTL


Ignore:
Timestamp:
Oct 14, 2011, 1:42:42 PM (8 years ago)
Author:
sacerdot
Message:

save_frame changed to accept also the formal/actual argument pairs, required
in the RTL semantics. The function returns now a res, but this could be fixed
with a dependent type for function call to disallow calling a function with the
wrong arguments.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/semantics.ma

    r1359 r1371  
    2222definition ltl_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    2323definition ltl_pop_frame: list beval → state … ltl_sem_params → res (state … ltl_sem_params) ≝ λ_.λst. OK … st.
    24 definition ltl_save_frame: unit → state … ltl_sem_params → state … ltl_sem_params ≝ λ_.λst.st.
     24definition ltl_save_frame: unit → nat → unit → state … ltl_sem_params → res (state … ltl_sem_params) ≝ λ_.λ_.λ_.λst.OK … st.
    2525
    2626definition ltl_more_sem_params1 : more_sem_params1 … ltl_params1 ≝
Note: See TracChangeset for help on using the changeset viewer.