`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.