Changeset 744 for src/Clight/Cexec.ma
 Timestamp:
 Apr 7, 2011, 6:53:59 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/Cexec.ma
r731 r744 345 345 #s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed. 346 346 347 definition eq_nat_dec : ∀n,m:nat. Sum (n=m) (n≠m). 348 #n #m lapply (refl ? (eqb n m)) cases (eqb n m) in ⊢ (???% → ?) #E 349 [ %1  %2 ] @(eqb_elim … E) // #_ #H destruct qed. 350 347 351 let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝ 348 352 match t1 return λt'. (t' = t2) + (t' ≠ t2) with … … 366 370 match eq_region_dec s s' with [ inl e1 ⇒ 367 371 match type_eq_dec t t' with [ inl e2 ⇒ 368 match decidable_eq_Z_Typen n' with [ inl e3 ⇒ inl ???372 match eq_nat_dec n n' with [ inl e3 ⇒ inl ??? 369 373  inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] 370 374  inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
Note: See TracChangeset
for help on using the changeset viewer.