Changeset 882 for src/Clight/TypeComparison.ma
 Timestamp:
 Jun 3, 2011, 5:35:32 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/TypeComparison.ma
r880 r882 13 13 definition eq_nat_dec : ∀n,m:nat. Sum (n=m) (n≠m). 14 14 #n #m lapply (refl ? (eqb n m)) cases (eqb n m) in ⊢ (???% → ?) #E 15 [ %1  %2 ] @(eqb_elim … E)// #_ #H destruct qed.15 [ %1  %2 ] lapply E @eqb_elim // #_ #H destruct qed. 16 16 17 17 let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
Note: See TracChangeset
for help on using the changeset viewer.