Major Section: ACL2-BUILT-INS
(intern symbol-name symbol-package-name) returns a symbol with
the given symbol-name and the given symbol-package-name. We
restrict Common Lisp's intern so that the second argument is
either the symbol *main-lisp-package-name*, the value of that
constant, or is one of "ACL2", "ACL2-INPUT-CHANNEL",
"ACL2-OUTPUT-CHANNEL", or "KEYWORD". To avoid that restriction,
see intern$.
In ACL2 intern is actually implemented as a macro that expands to
a call of a similar function whose second argument is a symbol.
Invoke :pe intern to see the definition, or
see intern-in-package-of-symbol.
To see why is intern so restricted consider
(intern "X" "P"). In particular, is it a symbol and if so,
what is its symbol-package-name? One is tempted to say ``yes, it
is a symbol in the package "P".'' But if package "P" has
not yet been defined, that would be premature because the imports to
the package are unknown. For example, if "P" were introduced
with
(defpkg "P" '(LISP::X))then in Common Lisp
(symbol-package-name (intern "X" "P")) returns
"LISP".The obvious restriction on intern is that its second argument be
the name of a package known to ACL2. We cannot express such a
restriction (except, for example, by limiting it to those packages
known at some fixed time, as we do). Instead, we provide
intern-in-package-of-symbol which requires a ``witness symbol''
for the package instead of the package. The witness symbol is any
symbol (expressible in ACL2) and uniquely specifies a package
necessarily known to ACL2.
