Changeset 744 for src/Clight/Cexec.ma


Ignore:
Timestamp:
Apr 7, 2011, 6:53:59 PM (10 years ago)
Author:
campbell
Message:

Evict Coq-style integers from common/Integers.ma.

Make more bitvector operations more efficient to retain the ability to
animate semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r731 r744  
    345345#s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
    346346
     347definition 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
    347351let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
    348352match t1 return λt'. (t' = t2) + (t' ≠ t2) with
     
    366370    match eq_region_dec s s' with [ inl e1 ⇒
    367371      match type_eq_dec t t' with [ inl e2 ⇒
    368         match decidable_eq_Z_Type n n' with [ inl e3 ⇒ inl ???
     372        match eq_nat_dec n n' with [ inl e3 ⇒ inl ???
    369373        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    370374        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
Note: See TracChangeset for help on using the changeset viewer.