Changeset 3542 for LTS


Ignore:
Timestamp:
Mar 18, 2015, 4:39:24 PM (5 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Lang_meas.ma

    r3540 r3542  
    128128          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    129129  ]
    130   cases daemon (*TODO*)
     130  #exp' #ltrue' #i_true' #lfalse' #i_false' #instrs'  #_ #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?);
     131  inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] * #a_top1 #istr1 #EQinstr'
     132  whd in ⊢ (??%%→ ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #a_top2 #istr2
     133  #EQi_false' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] *
     134  #a_top3 #istr3 #EQi_true' inversion(?==?) #EQget1 inversion(?==?) #EQget2 normalize nodelta
     135  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ #_ #EQ destruct % // * #f * #c #EQ destruct
    131136| cases daemon
    132137| cases daemon
Note: See TracChangeset for help on using the changeset viewer.