Changeset 3022 for src/correctness.ma


Ignore:
Timestamp:
Mar 28, 2013, 7:49:22 PM (7 years ago)
Author:
campbell
Message:

Make a couple of tests monadic for easier inversion.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r3021 r3022  
    126126#p_loc #EQ_assembler
    127127whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
     128
     129@('bind_inversion EQ_front_end) #cminor #CMINOR
     130#H @('bind_inversion H) -H #WCL #_
     131#H @('bind_inversion H) -H #INJ #_
     132#EQ_front_end'
     133
    128134#NOT_WRONG %
    129 [ cases daemon (* TODO *)
     135[ destruct cases daemon (* TODO *)
    130136| #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf
    131137
Note: See TracChangeset for help on using the changeset viewer.