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

Example Forms:
ACL2 !>(truncate 14 3)
ACL2 !>(truncate -14 3)
ACL2 !>(truncate 14 -3)
ACL2 !>(truncate -14 -3)
ACL2 !>(truncate -15 -3)
ACL2 !>(truncate 10/4 3/4)
(Truncate i j) is the result of taking the quotient of i and j and dropping the fraction. For example, the quotient of -14 by 3 is -4 2/3, so dropping the fraction 2/3, we obtain a result for (truncate -14 3) of -4.

The guard for (truncate i j) requires that i and j are 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.