Changeset 961 for src/common/Integers.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/common/Integers.ma

    r889 r961  
    436436#x #y change with (eq_bv ??? = eq_bv ???)
    437437 @eq_bv_elim @eq_bv_elim /2/
    438 [ #NE #E @False_ind >E in NE * /2/
    439 | #E #NE @False_ind >E in NE * /2/
    440 ] qed.
     438#E >E * #NE @False_ind @NE @refl
     439qed.
    441440
    442441theorem eq_spec: ∀x,y: int. if eq x y then x = y else (x ≠ y).
Note: See TracChangeset for help on using the changeset viewer.