Changeset 1599 for src/Clight/test/search.c.ma

Timestamp:

Dec 13, 2011, 1:34:37 AM (10 years ago)

Author:

sacerdot

Message:

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

File:

• src/Clight/test/search.c.ma (modified) (1 diff)

src/Clight/test/search.c.ma

@@ -215 +215 @@
 @refl
 qed.
+
+example csc: True.
+letin yyy ≝ (
+let xxx ≝ (clight_to_cminor myprog) in
+do p ← xxx ; cminor_to_rtlabs p)
+normalize in yyy;
+include "RTLabs/RTLabsToRTL.ma".
+
+example csc: True.
+letin xxx ≝ (clight_to_cminor myprog)
+letin yyy ≝ (do p ← xxx ; cminor_to_rtlabs p)
+letin zzz ≝ (do p ← yyy ; rtlabs_to_rtl p)
+@⊥ normalize in xxx;