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
jand returning the greatest integer not exceeding that quotient. For example, the quotient of
-4 2/3, and the largest integer not exceeding that rational number is
The guard for
(floor i j) requires that
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.