		Search-engine friendly clone of the ACL2 documentation.

Duplicate-detect

Vl-duplicate-detect-strip-modinst

Strip more from a vl-modinst for duplicate-detect.

Signature
(vl-duplicate-detect-strip-modinst x) → stripped-x
Arguments: x — Guard (vl-modinst-p x).
Returns: stripped-x — Type (vl-modinst-p stripped-x).

Definitions and Theorems

Function: vl-duplicate-detect-strip-modinst

(defun vl-duplicate-detect-strip-modinst (x)
  (declare (xargs :guard (vl-modinst-p x)))
  (let ((__function__ 'vl-duplicate-detect-strip-modinst))
    (declare (ignorable __function__))
    (change-vl-modinst (vl-modinst-strip x)
                       :instname nil
                       :str nil
                       :delay nil)))

Theorem: vl-modinst-p-of-vl-duplicate-detect-strip-modinst

(defthm vl-modinst-p-of-vl-duplicate-detect-strip-modinst
  (b* ((stripped-x (vl-duplicate-detect-strip-modinst x)))
    (vl-modinst-p stripped-x))
  :rule-classes :rewrite)