		Search-engine friendly clone of the ACL2 documentation.

Too-hard-to-propagate

Used-in-some-select-p

Signature
(used-in-some-select-p x) → names
Arguments: x — Guard (vl-module-p x).
Returns: names — Type (string-listp names), given the guard.

Definitions and Theorems

Function: used-in-some-select-p

(defun used-in-some-select-p (x)
  (declare (xargs :guard (vl-module-p x)))
  (let ((__function__ 'used-in-some-select-p))
    (declare (ignorable __function__))
    (b* ((exprs (vl-module-allexprs x))
         (selects (vl-exprlist-selects exprs))
         (names (vl-exprlist-names selects)))
      names)))

Theorem: string-listp-of-used-in-some-select-p

(defthm string-listp-of-used-in-some-select-p
  (implies (and (force (vl-module-p x)))
           (b* ((names (used-in-some-select-p x)))
             (string-listp names)))
  :rule-classes :rewrite)