		Search-engine friendly clone of the ACL2 documentation.

Symbol-package-name-lst

Lift symbol-package-name to lists.

Signature
(symbol-package-name-lst syms) → pkgs
Arguments: syms — Guard (symbol-listp syms).
Returns: pkgs — Type (string-listp pkgs).

This function is named similarly to the built-in symbol-name-lst.

Definitions and Theorems

Function: symbol-package-name-lst

(defun symbol-package-name-lst (syms)
       (declare (xargs :guard (symbol-listp syms)))
       (let ((__function__ 'symbol-package-name-lst))
            (declare (ignorable __function__))
            (cond ((endp syms) nil)
                  (t (cons (symbol-package-name (car syms))
                           (symbol-package-name-lst (cdr syms)))))))

Theorem: string-listp-of-symbol-package-name-lst

(defthm string-listp-of-symbol-package-name-lst
        (b* ((pkgs (symbol-package-name-lst syms)))
            (string-listp pkgs))
        :rule-classes :rewrite)

Theorem: len-of-symbol-package-name-lst

(defthm len-of-symbol-package-name-lst
        (b* ((?pkgs (symbol-package-name-lst syms)))
            (equal (len pkgs) (len syms))))