Intern
Create a new symbol in a given package
(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.
