		Search-engine friendly clone of the ACL2 documentation.

Floating-point-literal

Floating-point-literal-fix

Fixer for floating-point-literal.

Signature
(floating-point-literal-fix x) → fixed-x
Arguments: x — Guard (floating-point-literalp x).
Returns: fixed-x — Type (floating-point-literalp fixed-x).

Definitions and Theorems

Function: floating-point-literal-fix

(defun floating-point-literal-fix (x)
  (declare (xargs :guard (floating-point-literalp x)))
  (mbe :logic
       (if (floating-point-literalp x)
           x
         (floating-point-literal-witness))
       :exec x))

Theorem: floating-point-literalp-of-floating-point-literal-fix

(defthm floating-point-literalp-of-floating-point-literal-fix
  (b* ((fixed-x (floating-point-literal-fix x)))
    (floating-point-literalp fixed-x))
  :rule-classes :rewrite)

Theorem: floating-point-literal-fix-when-floating-point-literalp

(defthm floating-point-literal-fix-when-floating-point-literalp
  (implies (floating-point-literalp x)
           (equal (floating-point-literal-fix x)
                  x)))