Ignore:
Timestamp:
Jul 24, 2012, 7:40:13 PM (8 years ago)
Author:
campbell
Message:

Tweak Cminor invariant to be slightly more readable/extendable.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r2232 r2249  
    100100  ]
    101101  ]
    102 | whd in ⊢ (?(λ_.??(?(λ_.???%)?))?); >(no_labels … H) @(f_inv f)
     102| whd in match (labels_of ?); >(no_labels … H) @(f_inv f)
    103103] qed.
    104104
Note: See TracChangeset for help on using the changeset viewer.