symbol-package-name-lst

(in-package "ACL2")

(define symbol-package-name-lst
  ((syms symbol-listp))
  :returns (pkgs string-listp)
  :parents (std/basic)
  :short "Lift @(tsee symbol-package-name) to lists."
  :long (topstring (p "This function is named similarly to the built-in @('symbol-name-lst')."))
  (cond ((endp syms) nil)
    (t (cons (symbol-package-name (car syms))
        (symbol-package-name-lst (cdr syms)))))
  ///
  (defret len-of-symbol-package-name-lst
    (equal (len pkgs) (len syms))))