Ignore:
Timestamp:
Feb 16, 2011, 4:25:02 PM (8 years ago)
Author:
campbell
Message:

Minimal integration of bitvectors into Clight semantics

  • does a "round trip" through Z for most operations (slow)
  • a few extra bits for equality on vectors
  • version of reverse that doesn't make matita fall over on size 32 vectors during disambiguation and automation
File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/cerco/BitVector.ma

    r475 r535  
    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.