		Search-engine friendly clone of the ACL2 documentation.

Float-value-abs

Float-value-abs-fix

Fixer for float-value-abs.

Signature
(float-value-abs-fix x) → fixed-x
Arguments: x — Guard (float-value-abs-p x).
Returns: fixed-x — Type (float-value-abs-p fixed-x).

Definitions and Theorems

Function: float-value-abs-fix

(defun float-value-abs-fix (x)
  (declare (xargs :guard (float-value-abs-p x)))
  (mbe :logic
       (if (float-value-abs-p x)
           x
         (float-value-abs-pos-zero))
       :exec x))

Theorem: float-value-abs-p-of-float-value-abs-fix

(defthm float-value-abs-p-of-float-value-abs-fix
  (b* ((fixed-x (float-value-abs-fix x)))
    (float-value-abs-p fixed-x))
  :rule-classes :rewrite)

Theorem: float-value-abs-fix-when-float-value-abs-p

(defthm float-value-abs-fix-when-float-value-abs-p
  (implies (float-value-abs-p x)
           (equal (float-value-abs-fix x) x)))