Changeset 1599 for src/Clight/test/search.c.ma
- Timestamp:
- Dec 13, 2011, 1:34:37 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/test/search.c.ma
r1238 r1599 215 215 @refl 216 216 qed. 217 218 example csc: True. 219 letin yyy ≝ ( 220 let xxx ≝ (clight_to_cminor myprog) in 221 do p ← xxx ; cminor_to_rtlabs p) 222 normalize in yyy; 223 include "RTLabs/RTLabsToRTL.ma". 224 225 example csc: True. 226 letin xxx ≝ (clight_to_cminor myprog) 227 letin yyy ≝ (do p ← xxx ; cminor_to_rtlabs p) 228 letin zzz ≝ (do p ← yyy ; rtlabs_to_rtl p) 229 @⊥ normalize in xxx;
Note: See TracChangeset
for help on using the changeset viewer.