Ignore:
Timestamp:
Mar 8, 2013, 12:48:20 PM (8 years ago)
Author:
garnier
Message:

A consitent proof state for Clight to Cminor, with some progress (and some temporary regressions)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/frontend_misc.ma

    r2608 r2822  
    3939[ 1: #Heq destruct elim Hneq #Hcontr elim (Hcontr (refl ? t2))
    4040| 2: #Hneq' normalize // ] qed.
     41
     42lemma typ_eq_dec : ∀t1,t2:typ. (t1=t2)⊎(t1≠t2).
     43#t1 #t2
     44cases t1 cases t2
     45[ #sz #sg #sz' #sg' cases sz cases sz'
     46  try //
     47| #sz #sg %2 % #Habsurd destruct (Habsurd)
     48| #sz #sg %2 % #Habsurd destruct (Habsurd)
     49| %1 @refl ]
     50qed.
    4151
    4252lemma le_S_O_absurd : ∀x:nat. S x ≤ 0 → False. /2 by absurd/ qed.
Note: See TracChangeset for help on using the changeset viewer.