		Search-engine friendly clone of the ACL2 documentation.

Vl-make-paramdecloverrides

Vl-nonlocal-paramdecls

Filter parameter declarations, keeping only the non-local declarations.

Signature
(vl-nonlocal-paramdecls x) → nonlocal-params
Arguments: x — Guard (vl-paramdecllist-p x).
Returns: nonlocal-params — Type (vl-paramdecllist-p nonlocal-params).

Definitions and Theorems

Function: vl-nonlocal-paramdecls

(defun vl-nonlocal-paramdecls (x)
  (declare (xargs :guard (vl-paramdecllist-p x)))
  (let ((__function__ 'vl-nonlocal-paramdecls))
    (declare (ignorable __function__))
    (cond ((atom x) nil)
          ((vl-paramdecl->localp (car x))
           (vl-nonlocal-paramdecls (cdr x)))
          (t (cons (vl-paramdecl-fix (car x))
                   (vl-nonlocal-paramdecls (cdr x)))))))

Theorem: vl-paramdecllist-p-of-vl-nonlocal-paramdecls

(defthm vl-paramdecllist-p-of-vl-nonlocal-paramdecls
  (b* ((nonlocal-params (vl-nonlocal-paramdecls x)))
    (vl-paramdecllist-p nonlocal-params))
  :rule-classes :rewrite)

Theorem: vl-nonlocal-paramdecls-of-atom

(defthm vl-nonlocal-paramdecls-of-atom
  (implies (atom x)
           (equal (vl-nonlocal-paramdecls x) nil)))

Theorem: vl-nonlocal-paramdecls-of-cons

(defthm vl-nonlocal-paramdecls-of-cons
  (equal (vl-nonlocal-paramdecls (cons a x))
         (if (vl-paramdecl->localp a)
             (vl-nonlocal-paramdecls x)
           (cons (vl-paramdecl-fix a)
                 (vl-nonlocal-paramdecls x)))))

Theorem: vl-nonlocal-paramdecls-of-vl-paramdecllist-fix-x

(defthm vl-nonlocal-paramdecls-of-vl-paramdecllist-fix-x
  (equal (vl-nonlocal-paramdecls (vl-paramdecllist-fix x))
         (vl-nonlocal-paramdecls x)))

Theorem: vl-nonlocal-paramdecls-vl-paramdecllist-equiv-congruence-on-x

(defthm
      vl-nonlocal-paramdecls-vl-paramdecllist-equiv-congruence-on-x
  (implies (vl-paramdecllist-equiv x x-equiv)
           (equal (vl-nonlocal-paramdecls x)
                  (vl-nonlocal-paramdecls x-equiv)))
  :rule-classes :congruence)