SYMBOL-PACKAGE-NAME.html -- ACL2 Version 3.1

SYMBOL-PACKAGE-NAME

the name of the package of a symbol (a string)

Major Section:  PROGRAMMING

Completion Axiom:

(equal (symbol-package-name x)
       (if (symbolp x)
           (symbol-package-name x)
         ""))

Guard for (symbol-package-name x):

(symbolp x)

Note: If the ACL2 image is built on GCL, then symbol-package-name diverges from the name of the symbol's package in raw Lisp, in the case that this package is the main Lisp package. For example, (symbol-package-name 'car) evaluates to "COMMON-LISP" regardless of of the underlying Lisp implementation, even though the name of the main Lisp package in GCL is "LISP".