REM

remainder using 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.