Changeset 1515 for src/Clight/TypeComparison.ma
 Timestamp:
 Nov 18, 2011, 1:03:14 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/TypeComparison.ma
r1401 r1515 1 1 2 2 include "Clight/Csyntax.ma". 3 include "utilities/extranat.ma". 3 4 4 5 axiom TypeMismatch : String. … … 10 11 definition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2). 11 12 #s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed. 12 13 definition eq_nat_dec : ∀n,m:nat. Sum (n=m) (n≠m).14 #n #m lapply (refl ? (eqb n m)) cases (eqb n m) in ⊢ (???% → ?) #E15 [ %1  %2 ] lapply E @eqb_elim // #_ #H destruct qed.16 13 17 14 let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
Note: See TracChangeset
for help on using the changeset viewer.