Changeset 700 for src/ASM


Ignore:
Timestamp:
Mar 18, 2011, 4:28:26 PM (10 years ago)
Author:
campbell
Message:

Get Clight semantics going again (except for problems CexecEquiv? that I caused
earlier).

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVector.ma

    r698 r700  
    123123        false) b c.
    124124
    125 (* dpm: commented out to get our stuff to typecheck
    126125lemma eq_bv_elim: ∀P:bool → Prop. ∀n. ∀x,y.
    127126  (x = y → P true) →
     
    131130#Q * *; normalize /3/
    132131qed.
    133 *)
    134132
    135133let rec bitvector_of_nat (n: nat) (m: nat): BitVector n ≝
  • src/ASM/BitVectorZ.ma

    r697 r700  
    11
    2 include "binary/Z.ma".
    3 include "cerco/BitVector.ma".
    4 include "cerco/Arithmetic.ma".
     2include "utilities/binary/Z.ma".
     3include "ASM/BitVector.ma".
     4include "ASM/Arithmetic.ma".
    55
    66let rec Z_of_unsigned_bitvector (n:nat) (bv:BitVector n) on bv : Z ≝
  • src/ASM/Vector.ma

    r698 r700  
    1212include "arithmetics/nat.ma".
    1313
    14 (* include "oldlib/eq.ma". *)
     14include "utilities/oldlib/eq.ma".
    1515
    1616(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    469469*)
    470470
    471 (* dpm: commented out to get out stuff to typecheck
     471(* dpm: commented out to get out stuff to typecheck *)
    472472lemma eq_v_elim: ∀P:bool → Prop. ∀A,f.
    473473  (∀Q:bool → Prop. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) →
     
    486486  ]
    487487] qed.
    488 *)
    489488
    490489(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.