ROUND

division returning an integer by rounding off 
Major Section:  PROGRAMMING


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.