division returning an integer by truncating toward negative infinity
Major Section:  ACL2-BUILT-INS

Example Forms:
ACL2 !>(floor 14 3)
ACL2 !>(floor -14 3)
ACL2 !>(floor 14 -3)
ACL2 !>(floor -14 -3)
ACL2 !>(floor -15 -3)
(Floor i j) returns the result of taking the quotient of i and j and returning the greatest integer not exceeding that quotient. For example, the quotient of -14 by 3 is -4 2/3, and the largest integer not exceeding that rational number is -5.

The guard for (floor i j) requires that i and j are rational (real, in ACL2(r)) numbers and j is non-zero.

Floor is a Common Lisp function. See any Common Lisp documentation for more information. However, note that unlike Common Lisp, the ACL2 floor function returns only a single value,

To see the ACL2 definition of this function, see pf.