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

SYMBOL-PACKAGE-NAME

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

Major Section:  ACL2-BUILT-INS

WARNING: While symbol-package-name behaves properly on all ACL2 objects, it may give surprising results when called in raw Lisp. For more details see pkg-imports, in particular the discussion there of the "COMMON-LISP" package.

Completion Axiom (completion-of-symbol-package-name):

(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".