Mod is a Common Lisp function. See any Common Lisp documentation
for more information.
floor
Major Section: PROGRAMMING
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.