`truncate`

Major Section: ACL2-BUILT-INS

ACL2 !>(rem 14 3) 2 ACL2 !>(rem -14 3) -2 ACL2 !>(rem 14 -3) 2 ACL2 !>(rem -14 -3) -2 ACL2 !>(rem -15 -3) 0 ACL2 !>

`(Rem i j)`

is that number `k`

for which `(* j (truncate i j))`

added
to `k`

equals `i`

.
The guard for `(rem i j)`

requires that `i`

and `j`

are rational
(real, in ACL2(r)) numbers and `j`

is non-zero.

`Rem`

is a Common Lisp function. See any Common Lisp documentation
for more information.

To see the ACL2 definition of this function, see pf.