		Search-engine friendly clone of the ACL2 documentation.

4vmask

4vmask-fix

Fixing function for 4vmasks.

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

This is unlike ifix because we return -1 (``all bits are relevant'') in the default case.

Definitions and Theorems

Function: 4vmask-fix$inline

(defun 4vmask-fix$inline (x)
  (declare (xargs :guard (4vmask-p x)))
  (let ((__function__ '4vmask-fix))
    (declare (ignorable __function__))
    (mbe :logic (if (4vmask-p x) x -1)
         :exec x)))

Theorem: 4vmask-p-of-4vmask-fix

(defthm 4vmask-p-of-4vmask-fix
  (b* ((x-fix (4vmask-fix$inline x)))
    (4vmask-p x-fix))
  :rule-classes (:rewrite :type-prescription))

Theorem: 4vmask-fix-when-4vmask-p

(defthm 4vmask-fix-when-4vmask-p
  (implies (4vmask-p x)
           (equal (4vmask-fix x) x)))