Changeset 726 for src/Clight/AST.ma


Ignore:
Timestamp:
Mar 30, 2011, 6:47:35 PM (10 years ago)
Author:
campbell
Message:

Change identifiers to Words in Clight and RTLabs semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/AST.ma

    r718 r726  
    2121include "common/Integers.ma".
    2222include "common/Floats.ma".
    23 include "utilities/binary/positive.ma".
     23include "ASM/BitVector.ma".
    2424
    2525(* * * Syntactic elements *)
     
    2828  etc) are represented by the type [positive] of positive integers. *)
    2929
    30 definition ident ≝ Pos.
     30definition ident ≝ Word.
    3131
    3232definition 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 ]
     35lapply E @eq_bv_elim
     36[ 1,4: #H #_ @H | *: #_ #H destruct ]
     37qed.
     38
     39definition ident_of_nat ≝ bitvector_of_nat 16.
    3540
    3641(* Memory spaces *)
Note: See TracChangeset for help on using the changeset viewer.