		Search-engine friendly clone of the ACL2 documentation.

4vec

4vec-fix

Fix an arbitrary object to a 4vec.

Signature
(4vec-fix x) → newx
Arguments: x — Guard (4vec-p x).
Returns: newx — Type (4vec-p newx).

Definitions and Theorems

Function: 4vec-fix$inline

(defun 4vec-fix$inline (x)
  (declare (xargs :guard (4vec-p x)))
  (let ((__function__ '4vec-fix))
    (declare (ignorable __function__))
    (mbe :logic
         (if (consp x)
             (4vec (ifix (car x)) (ifix (cdr x)))
           (if (integerp x) x (4vec-x)))
         :exec x)))

Theorem: 4vec-p-of-4vec-fix

(defthm 4vec-p-of-4vec-fix
  (b* ((newx (4vec-fix$inline x)))
    (4vec-p newx))
  :rule-classes :rewrite)

Theorem: 4vec-fix-of-4vec

(defthm 4vec-fix-of-4vec
  (implies (4vec-p x)
           (equal (4vec-fix x) x)))