Symbol-package-name
The name of the package of a symbol (a string)
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: Symbol-package-name may diverge from the name of the symbol's
package in raw Lisp, in the case that this package is the main Lisp package.
For example, in GCL (symbol-package-name 'car) evaluates to
"COMMON-LISP" even though the actual package name for the symbol, car,
is "LISP".
