		Search-engine friendly clone of the ACL2 documentation.

Strict-opcode-fix

Signature
(strict-opcode-fix x) → *
Arguments: x — Guard (strict-opcode-p x).

Definitions and Theorems

Function: strict-opcode-fix

(defun strict-opcode-fix (x)
  (declare (xargs :guard (strict-opcode-p x)))
  (let ((__function__ 'strict-opcode-fix))
    (declare (ignorable __function__))
    (if (strict-opcode-p x)
        x
      (b* ((x (opcode-fix x))
           (x (change-opcode x :feat nil)))
        x))))