		Search-engine friendly clone of the ACL2 documentation.

Logops-definitions

Ifloor

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

Signature
(ifloor 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: ifloor$inline

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

Theorem: ifloor-type

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