		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-queries

All-pkg-names

Collect all the package names of all the symbols in a term.

Signature
(all-pkg-names term) → pkg-names
Arguments: term — Guard (pseudo-termp term).
Returns: pkg-names — Type (string-listp pkg-names).

Function: all-pkg-names

(defun all-pkg-names (term)
 (declare (xargs :guard (pseudo-termp term)))
 (let ((__function__ 'all-pkg-names))
  (declare (ignorable __function__))
  (cond
   ((variablep term)
    (list (symbol-package-name term)))
   ((fquotep term)
    (if (symbolp (cadr term))
        (list (symbol-package-name (cadr term)))
      nil))
   ((symbolp (ffn-symb term))
    (add-to-set-equal (symbol-package-name (ffn-symb term))
                      (all-pkg-names-lst (fargs term))))
   (t
    (union-equal
     (remove-duplicates-equal
         (symbol-package-name-lst (lambda-formals (ffn-symb term))))
     (union-equal (all-pkg-names (lambda-body (ffn-symb term)))
                  (all-pkg-names-lst (fargs term))))))))

Function: all-pkg-names-lst

(defun all-pkg-names-lst (terms)
  (declare (xargs :guard (pseudo-term-listp terms)))
  (let ((__function__ 'all-pkg-names-lst))
    (declare (ignorable __function__))
    (cond ((endp terms) nil)
          (t (union-equal (all-pkg-names (car terms))
                          (all-pkg-names-lst (cdr terms)))))))

Theorem: return-type-of-all-pkg-names.pkg-names

(defthm return-type-of-all-pkg-names.pkg-names
  (b* ((?pkg-names (all-pkg-names term)))
    (string-listp pkg-names))
  :rule-classes :rewrite)

Theorem: return-type-of-all-pkg-names-lst.pkg-names

(defthm return-type-of-all-pkg-names-lst.pkg-names
  (b* ((?pkg-names (all-pkg-names-lst terms)))
    (string-listp pkg-names))
  :rule-classes :rewrite)

Subtopics

All-pkg-names-lst