Changeset 3583
- Timestamp:
- Jul 16, 2015, 5:09:09 PM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/variable_stack_pass.ma
r3582 r3583 442 442 var_to_shift_ok (\fst st) → frame_assign_var st v val = return new_st → 443 443 var_to_shift_ok (\fst new_st). 444 cases daemon 444 ** [|#x #xs] #fp #v #val #new_st * [| #H1 #H2] whd in ⊢ (??%% → ?); [ #EQ destruct] 445 whd 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) // 445 448 qed. 446 449
Note: See TracChangeset
for help on using the changeset viewer.