Changeset 3582 for LTS/Language.ma


Ignore:
Timestamp:
Jul 16, 2015, 4:02:53 PM (4 years ago)
Author:
piccolo
Message:

pass variable to stack in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3579 r3582  
    247247| empty : ∀st,st',hd,tl.(code ? st) = (EMPTY p p)→ (cont ? st) = hd :: tl →
    248248           (code ? st') = \snd hd → (cont … st') = tl → (store … st) = (store … st') →
    249            (io_info … st = true → is_non_silent_cost_act … (\fst hd)) →  (io_info … st') = false → ¬ is_ret_call_act … (\fst hd) →  execute_l … (\fst hd) st st'
     249           (io_info … st = true → is_non_silent_cost_act … (\fst hd)) →  (io_info … st') = false → is_cost_label … (\fst hd) →  execute_l … (\fst hd) st st'
    250250| seq_sil : ∀st,st',i,cd,s,opt_l.(code ? st) = SEQ … i opt_l cd →
    251251             eval_seq … p' i (store … st) = return s → (code ? st') = cd →
Note: See TracChangeset for help on using the changeset viewer.