		Search-engine friendly clone of the ACL2 documentation.

Mod

Remainder using floor

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.

Function: mod

(defun mod (x y)
  (declare (xargs :guard (and (real/rationalp x)
                              (real/rationalp y)
                              (not (eql y 0)))))
  (- x (* (floor x y) y)))