Ignore:
Timestamp:
Dec 13, 2011, 1:34:37 AM (8 years ago)
Author:
sacerdot
Message:

Start of merging of stuff into the standard library of Matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/search.c.ma

    r1238 r1599  
    215215@refl
    216216qed.
     217
     218example csc: True.
     219letin yyy ≝ (
     220let xxx ≝ (clight_to_cminor myprog) in
     221do p ← xxx ; cminor_to_rtlabs p)
     222normalize in yyy;
     223include "RTLabs/RTLabsToRTL.ma".
     224
     225example csc: True.
     226letin xxx ≝ (clight_to_cminor myprog)
     227letin yyy ≝ (do p ← xxx ; cminor_to_rtlabs p)
     228letin zzz ≝ (do p ← yyy ; rtlabs_to_rtl p)
     229@⊥ normalize in xxx;
Note: See TracChangeset for help on using the changeset viewer.