### ROUND

division returning an integer by rounding off
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.