|
|
|---|
|
|
|
|---|
Fixtype of symbol values.
This is a product type introduced by fty::defprod.
Conceptually, a symbol consists of a package name and a (symbol) name.
We do not use the fixtype of the ACL2 symbols here (i.e. the fixtype for the built-in recognizer symbolp), because that type only contains symbols with known package names. Here instead we are formalizing the ACL2 programming language at the meta level, and therefore we must be able to talk about all possible symbols for different collections of known packages.
We use any strings as package names, even though there are restrictions on package names (see defpkg). These restrictions may be formalized elsewhere.