Changeset 726 for src/Clight/AST.ma
 Timestamp:
 Mar 30, 2011, 6:47:35 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/AST.ma
r718 r726 21 21 include "common/Integers.ma". 22 22 include "common/Floats.ma". 23 include " utilities/binary/positive.ma".23 include "ASM/BitVector.ma". 24 24 25 25 (* * * Syntactic elements *) … … 28 28 etc) are represented by the type [positive] of positive integers. *) 29 29 30 definition ident ≝ Pos.30 definition ident ≝ Word. 31 31 32 32 definition ident_eq : ∀x,y:ident. (x=y) + (x≠y). 33 #x #y lapply (pos_compare_to_Prop x y); cases (pos_compare x y); 34 [ #H %2 /2/;  #H %1 //;  #H %2 /2/ ] qed. 33 #x #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → %) #E 34 [ %  %2 ] 35 lapply E @eq_bv_elim 36 [ 1,4: #H #_ @H  *: #_ #H destruct ] 37 qed. 38 39 definition ident_of_nat ≝ bitvector_of_nat 16. 35 40 36 41 (* Memory spaces *)
Note: See TracChangeset
for help on using the changeset viewer.