### FLOOR

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

Example Forms:
ACL2 !>(floor 14 3)
4
ACL2 !>(floor -14 3)
-5
ACL2 !>(floor 14 -3)
-5
ACL2 !>(floor -14 -3)
4
ACL2 !>(floor -15 -3)
5

`(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.