		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Vl-delete-sd-problems-for-modnames

Signature
(vl-delete-sd-problems-for-modnames names probs) → new-x
Arguments: names — Guard (string-listp names).; probs — Guard (sd-problemlist-p probs).
Returns: new-x — Type (sd-problemlist-p new-x), given (force (sd-problemlist-p probs)).

Definitions and Theorems

Function: vl-delete-sd-problems-for-modnames

(defun vl-delete-sd-problems-for-modnames (names probs)
  (declare (xargs :guard (and (string-listp names)
                              (sd-problemlist-p probs))))
  (let ((__function__ 'vl-delete-sd-problems-for-modnames))
    (declare (ignorable __function__))
    (b* ((fal (make-lookup-alist names))
         (ret (vl-delete-sd-problems-for-modnames-aux fal probs)))
      (fast-alist-free fal)
      ret)))

Theorem: sd-problemlist-p-of-vl-delete-sd-problems-for-modnames

(defthm sd-problemlist-p-of-vl-delete-sd-problems-for-modnames
 (implies
      (force (sd-problemlist-p probs))
      (b* ((new-x (vl-delete-sd-problems-for-modnames names probs)))
        (sd-problemlist-p new-x)))
 :rule-classes :rewrite)