Major Section: ACL2-BUILT-INS
For any string pkg that names a package currently known to ACL2,
(pkg-witness pkg) is a symbol in that package whose symbol-name is
the value of constant *pkg-witness-name*. Logically, this is the case
even if the package is not currently known to ACL2. However, if
pkg-witness is called on a string that is not the name of a package known
to ACL2, a hard Lisp error will result.
(Pkg-witness pkg) has a guard of
(and (stringp pkg) (not (equal pkg ""))). If pkg is not a string,
then (pkg-witness pkg) is equal to (pkg-witness "ACL2")
