		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Vl-delete-sd-problems-for-modnames-aux

Signature
(vl-delete-sd-problems-for-modnames-aux fal x) → new-x
Arguments: fal — Fast alist binding names to T or whatever.; x — Guard (sd-problemlist-p x).
Returns: new-x — Type (sd-problemlist-p new-x), given the guard.

Definitions and Theorems

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

(defun vl-delete-sd-problems-for-modnames-aux (fal x)
  (declare (xargs :guard (sd-problemlist-p x)))
  (let ((__function__ 'vl-delete-sd-problems-for-modnames-aux))
    (declare (ignorable __function__))
    (b* (((when (atom x)) nil)
         ((sd-problem x1) (car x))
         ((vl-context1 x1.ctx) x1.ctx)
         ((when (hons-get x1.ctx.mod fal))
          (vl-delete-sd-problems-for-modnames-aux fal (cdr x))))
      (cons (car x)
            (vl-delete-sd-problems-for-modnames-aux fal (cdr x))))))

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

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