Major Section: ACL2-BUILT-INS
Example Forms: ACL2 !>(ceiling 14 3) 5 ACL2 !>(ceiling -14 3) -4 ACL2 !>(ceiling 14 -3) -4 ACL2 !>(ceiling -14 -3) 5 ACL2 !>(ceiling -15 -3) 5
(Ceiling i j) is the result of taking the quotient of i and
j and returning the smallest integer that is at least as great as
that quotient. For example, the quotient of -14 by 3 is -4 2/3, and
the smallest integer at least that great is -4.
The guard for (ceiling i j) requires that i and j are
rational (real, in ACL2(r)) numbers and j is non-zero.
Ceiling is a Common Lisp function. See any Common Lisp documentation for
more information. However, note that unlike Common Lisp, the ACL2
ceiling function returns only a single value,
To see the ACL2 definition of this function, see pf.
