Ignore:
Timestamp:
Nov 18, 2011, 1:03:14 PM (9 years ago)
Author:
campbell
Message:

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/TypeComparison.ma

    r1401 r1515  
    11
    22include "Clight/Csyntax.ma".
     3include "utilities/extranat.ma".
    34
    45axiom TypeMismatch : String.
     
    1011definition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
    1112#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 ⊢ (???% → ?) #E
    15 [ %1 | %2 ] lapply E @eqb_elim // #_ #H destruct qed.
    1613
    1714let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
Note: See TracChangeset for help on using the changeset viewer.