		Search-engine friendly clone of the ACL2 documentation.

Std/basic

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))))