Changeset 697 for src/ASM/BitVector.ma


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

Merge Clight branch of vectors and friends.
Start making stuff build.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM

  • src/ASM/BitVector.ma

    r690 r697  
    123123        false) b c.
    124124
     125lemma eq_bv_elim: ∀P:bool → Prop. ∀n. ∀x,y.
     126  (x = y → P true) →
     127  (x ≠ y → P false) →
     128  P (eq_bv n x y).
     129#P #n #x #y #Ht #Hf whd in ⊢ (?%) @(eq_v_elim … Ht Hf)
     130#Q * *; normalize /3/
     131qed.
     132
    125133let rec bitvector_of_nat (n: nat) (m: nat): BitVector n ≝
    126134  let biglist ≝ rev ? (bitvector_of_nat_aux m m) in
Note: See TracChangeset for help on using the changeset viewer.