Major Section: ACL2-BUILT-INS
Example Forms: ACL2 !>(round 14 3) 5 ACL2 !>(round -14 3) -5 ACL2 !>(round 14 -3) -5 ACL2 !>(round -14 -3) 5 ACL2 !>(round 13 3) 4 ACL2 !>(round -13 3) -4 ACL2 !>(round 13 -3) -4 ACL2 !>(round -13 -3) 4 ACL2 !>(round -15 -3) 5 ACL2 !>(round 15 -2) -8
(Round i j) is the result of taking the quotient of i and j
and rounding off to the nearest integer. When the quotient is
exactly halfway between consecutive integers, it rounds to the even
one.
The guard for (round i j) requires that i and j are
rational (real, in ACL2(r)) numbers and j is non-zero.
Round is a Common Lisp function. See any Common Lisp documentation for
more information. However, note that unlike Common Lisp, the ACL2 round
function returns only a single value,
To see the ACL2 definition of this function, see pf.
