MOD

remainder using floor
Major Section:  ACL2-BUILT-INS

ACL2 !>(mod 14 3)
2
ACL2 !>(mod -14 3)
1
ACL2 !>(mod 14 -3)
-1
ACL2 !>(mod -14 -3)
-2
ACL2 !>(mod -15 -3)
0
ACL2 !>
(Mod i j) is that number k that (* j (floor i j)) added to k equals i.

The guard for (mod i j) requires that i and j are rational (real, in ACL2(r)) numbers and j is non-zero.

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

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