Changeset 3593


Ignore:
Timestamp:
Jul 25, 2015, 6:34:19 PM (4 years ago)
Author:
pellitta
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/variable_stack_pass.ma

    r3592 r3593  
    476476#act_frm (* [|#x #xs]*) #i #seq #ol #ct whd in ⊢(%→?);
    477477<(append_nil … [?]) >divide_continuation_on_frame_app
    478 inversion(divide_continuation_on_frames ct ?)
    479 normalize nodelta [2,4: #x #xs #_] #EQdivide
    480 
    481 cases act_frm -act_frm [2,4: #y #ys] **
     478inversion(divide_continuation_on_frames ct ?) normalize nodelta
     479[2,4: #x #xs #_] #EQdivide cases act_frm -act_frm [2,4: #y #ys] **
    482480#H1 #H2 #H3 whd in match (var_instr_bond_ok ???);
    483481<(append_nil … [?]) >divide_continuation_on_frame_app >EQdivide normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.