Major Section: ACL2-BUILT-INS
Example Forms: ACL2 !>(truncate 14 3) 4 ACL2 !>(truncate -14 3) -4 ACL2 !>(truncate 14 -3) -4 ACL2 !>(truncate -14 -3) 4 ACL2 !>(truncate -15 -3) 5 ACL2 !>(truncate 10/4 3/4) 3
(Truncate i j)is the result of taking the quotient of
jand dropping the fraction. For example, the quotient of
-4 2/3, so dropping the fraction
2/3, we obtain a result for
(truncate -14 3)of
The guard for
(truncate i j) requires that
rational (real, in ACL2(r)) numbers and
j is non-zero.
Truncate is a Common Lisp function. However, note that unlike Common
Lisp, the ACL2
truncate function returns only a single value, Also
see nonnegative-integer-quotient, which is appropriate for integers and may
simplify reasoning, unless a suitable arithmetic library is loaded, but be
less efficient for evaluation on concrete objects.
To see the ACL2 definition of this function, see pf.