		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Maybe-integer

Signature
(maybe-integer i x intp) → *
Arguments: i — Guard (integerp i).

Definitions and Theorems

Function: maybe-integer

(defun maybe-integer (i x intp)
  (declare (xargs :guard (integerp i)))
  (let ((__function__ 'maybe-integer))
    (declare (ignorable __function__))
    (if intp (ifix i) (non-int-fix x))))

Theorem: maybe-integer-t

(defthm maybe-integer-t
  (equal (maybe-integer i x t) (ifix i)))

Theorem: maybe-integer-nil

(defthm maybe-integer-nil
  (equal (maybe-integer i x nil)
         (non-int-fix x)))