Major Section: PROGRAMMING
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.