Changeset 16 for C-semantics/extralib.ma


Ignore:
Timestamp:
Jul 26, 2010, 5:19:31 PM (9 years ago)
Author:
campbell
Message:

Add rest of the expressions to executable Clight semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/extralib.ma

    r15 r16  
    3131nlemma eq_rect_Type2_r:
    3232 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
     33 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r2 ??? p0); nassumption.
     34nqed.
     35
     36nlemma eq_rect_CProp0_r:
     37 ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
    3338 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r2 ??? p0); nassumption.
    3439nqed.
Note: See TracChangeset for help on using the changeset viewer.