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
jand 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
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
function returns only a single value,
To see the ACL2 definition of this function, see pf.