Changeset 961 for src/ASM/BitVector.ma


Ignore:
Timestamp:
Jun 15, 2011, 4:15:52 PM (8 years ago)
Author:
campbell
Message:

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVector.ma

    r868 r961  
    110110#Q * *; normalize /3/
    111111qed.
     112
     113lemma eq_bv_true: ∀n,v. eq_bv n v v = true.
     114@eq_v_true * @refl
     115qed.
     116
     117lemma eq_bv_false: ∀n,v,v'. v ≠ v' → eq_bv n v v' = false.
     118#n #v #v' #NE @eq_v_false [ * * #H try @refl normalize in H; destruct | @NE ]
     119qed.
    112120   
    113121axiom bitvector_of_string:
Note: See TracChangeset for help on using the changeset viewer.