Changeset 744 for src/utilities
 Timestamp:
 Apr 7, 2011, 6:53:59 PM (10 years ago)
 Location:
 src/utilities
 Files:

 1 added
 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/Coqlib.ma
r697 r744 23 23 24 24 include "utilities/extralib.ma". 25 include "ASM/Util.ma". 25 26 26 27 (* … … 576 577 (*naxiom align : Z → Z → Z.*) 577 578 578 definition align ≝ λn: Z. λamount: Z.579 (( n + amount  1) /amount) * amount.579 definition align : nat → nat → nat ≝ λn: nat. λamount: nat. 580 ((minus (n + amount) 1) ÷ amount) * amount. 580 581 (* 581 582 Lemma align_le: forall x y, y > 0 > x <= align x y.
Note: See TracChangeset
for help on using the changeset viewer.