		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Non-int-fix

Identity for non-integers; coerces any integers to nil.

Signature
(non-int-fix x) → *

Definitions and Theorems

Function: non-int-fix

(defun non-int-fix (x)
  (declare (xargs :guard t))
  (let ((__function__ 'non-int-fix))
    (declare (ignorable __function__))
    (and (not (integerp x)) x)))

Theorem: non-int-fix-when-non-integer

(defthm non-int-fix-when-non-integer
  (implies (not (integerp x))
           (equal (non-int-fix x) x))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))