Ignore:
Timestamp:
Apr 7, 2011, 6:53:59 PM (10 years ago)
Author:
campbell
Message:

Evict Coq-style integers from common/Integers.ma.

Make more bitvector operations more efficient to retain the ability to
animate semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/Coqlib.ma

    r697 r744  
    2323
    2424include "utilities/extralib.ma".
     25include "ASM/Util.ma".
    2526
    2627(*
     
    576577(*naxiom align : Z → Z → Z.*)
    577578
    578 definition align ≝ λn: Z. λamount: Z.
    579   ((n + amount - 1) / amount) * amount.
     579definition align : nat → nat → nat ≝ λn: nat. λamount: nat.
     580  ((minus (n + amount) 1) ÷ amount) * amount.
    580581(*
    581582Lemma align_le: forall x y, y > 0 -> x <= align x y.
Note: See TracChangeset for help on using the changeset viewer.