### TRUNCATE

division returning an integer by truncating toward 0
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 `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.