		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Vl-remove-nameless-descriptions

Signature
(vl-remove-nameless-descriptions x) → new-x
Arguments: x — Guard (vl-descriptionlist-p x).
Returns: new-x — Type (vl-descriptionlist-p new-x).

Definitions and Theorems

Function: vl-remove-nameless-descriptions

(defun vl-remove-nameless-descriptions (x)
  (declare (xargs :guard (vl-descriptionlist-p x)))
  (let ((__function__ 'vl-remove-nameless-descriptions))
    (declare (ignorable __function__))
    (cond ((atom x) nil)
          ((not (vl-description->origname (car x)))
           (vl-remove-nameless-descriptions (cdr x)))
          (t (cons (vl-description-fix (car x))
                   (vl-remove-nameless-descriptions (cdr x)))))))

Theorem: vl-descriptionlist-p-of-vl-remove-nameless-descriptions

(defthm vl-descriptionlist-p-of-vl-remove-nameless-descriptions
  (b* ((new-x (vl-remove-nameless-descriptions x)))
    (vl-descriptionlist-p new-x))
  :rule-classes :rewrite)