Changeset 3567 for LTS


Ignore:
Timestamp:
Jun 17, 2015, 4:29:24 PM (4 years ago)
Author:
sacerdot
Message:

Actual parameters fixed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/variable.ma

    r3566 r3567  
    7676|@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality)
    7777|@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality)
    78 |@(DeqProd variable DeqExpr)
     78|@DeqExpr
    7979|@DeqExpr].qed.
    8080
     
    117117definition frame_eval_call:(signature frame_state_params frame_state_params)→ act_params_type frame_state_params → frame_store_t → (option frame_store_t)≝
    118118λsgn,e,st.
    119     let 〈var,act_exp〉 ≝ e in
    120119    !env ← frame_current_env … st;
    121     !n ← frame_sem_expr env act_exp;
     120    !n ← frame_sem_expr env e;
    122121    frame_assign_var 〈((nil ?)::(\fst st)),(\snd st)〉 to_shift n.
    123122
Note: See TracChangeset for help on using the changeset viewer.