Changeset 16 for C-semantics/extralib.ma

Timestamp:

Jul 26, 2010, 5:19:31 PM (10 years ago)

Author:

campbell

Message:

Add rest of the expressions to executable Clight semantics.

File:

• C-semantics/extralib.ma (modified) (1 diff)

C-semantics/extralib.ma

@@ -31 +31 @@
 nlemma eq_rect_Type2_r:
  ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r2 ??? p0); nassumption.
+nqed.
+
+nlemma eq_rect_CProp0_r:
+ ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
  #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r2 ??? p0); nassumption.
 nqed.