Changeset 700 for src/ASM/BitVector.ma


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

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

File:
1 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 ≝
Note: See TracChangeset for help on using the changeset viewer.