		Search-engine friendly clone of the ACL2 documentation.

Logops-definitions

Imod

(imod i j) is the same as mod, except that it coerces its arguments to integers.

Signature
(imod i j) → int
Arguments: i — Guard (integerp i).; j — Guard (and (integerp j) (not (= 0 j))).
Returns: int — Type (integerp int).

Definitions and Theorems

Function: imod$inline

(defun
     imod$inline (i j)
     (declare (xargs :guard (and (integerp i)
                                 (and (integerp j) (not (= 0 j))))))
     (let ((__function__ 'imod))
          (declare (ignorable __function__))
          (mbe :logic (mod (ifix i) (ifix j))
               :exec (mod i j))))

Theorem: imod-type

(defthm imod-type
        (b* ((int (imod$inline i j)))
            (integerp int))
        :rule-classes :type-prescription)