Truncate is a Common Lisp function. However, note that unlike Common
Lisp, the ACL2 truncate function returns only a single value,
Major Section: PROGRAMMING
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
(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,