		Search-engine friendly clone of the ACL2 documentation.

Uint-integer-fix

Fixer for uint-integer.

Function: uint-integer-fix

(defun uint-integer-fix (x)
  (declare (xargs :guard (uint-integerp x)))
  (mbe :logic (if (uint-integerp x) x 0)
       :exec x))

Theorem: uint-integerp-of-uint-integer-fix

(defthm uint-integerp-of-uint-integer-fix
  (b* ((fixed-x (uint-integer-fix x)))
    (uint-integerp fixed-x))
  :rule-classes :rewrite)

Theorem: uint-integer-fix-when-uint-integerp

(defthm uint-integer-fix-when-uint-integerp
  (implies (uint-integerp x)
           (equal (uint-integer-fix x) x)))