		Search-engine friendly clone of the ACL2 documentation.

Vl-description

Vl-slow-delete-descriptions

Signature
(vl-slow-delete-descriptions names x) → *
Arguments: names — Guard (string-listp names).; x — Guard (vl-descriptionlist-p x).

Definitions and Theorems

Function: vl-slow-delete-descriptions

(defun vl-slow-delete-descriptions (names x)
  (declare (xargs :guard (and (string-listp names)
                              (vl-descriptionlist-p x))))
  (let ((__function__ 'vl-slow-delete-descriptions))
    (declare (ignorable __function__))
    (cond ((atom x) nil)
          ((member-equal (vl-description->name (car x))
                         (string-list-fix names))
           (vl-slow-delete-descriptions names (cdr x)))
          (t (cons (vl-description-fix (car x))
                   (vl-slow-delete-descriptions names (cdr x)))))))