Changeset 3583


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

closed first daemon

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/variable_stack_pass.ma

    r3582 r3583  
    442442var_to_shift_ok (\fst st) → frame_assign_var st v val = return new_st →
    443443var_to_shift_ok (\fst new_st).
    444 cases daemon
     444** [|#x #xs] #fp #v #val #new_st * [| #H1 #H2] whd in ⊢ (??%% → ?); [ #EQ destruct]
     445whd in match assign_frame; normalize nodelta inversion(update  …) normalize nodelta
     446[ #_ #EQ destruct] #new_frm #EQnew_frm whd in ⊢ (??%% → ?); #EQ destruct % //
     447@(transitive_le … H1) >(len_update … x … EQnew_frm) //
    445448qed.
    446449
Note: See TracChangeset for help on using the changeset viewer.