Changeset 3585


Ignore:
Timestamp:
Jul 18, 2015, 5:42:18 PM (4 years ago)
Author:
pellitta
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/variable_stack_pass.ma

    r3584 r3585  
    458458frame_assign_var st v val = return new_st →
    459459var_instr_bond_ok (\fst new_st) i ct.
     460** [|#x #xs] #fp #i #ct #v #val #new_st whd in ⊢(%→?→?);
     461inversion(divide_continuation_on_frames ct [i])
     462#IH normalize nodelta whd in ⊢(?→%→%); [#_|3:#ABS cases ABS]
     463[>IH whd in match (frame_assign_var ???); #HN
    460464cases daemon
    461465qed.
Note: See TracChangeset for help on using the changeset viewer.