Major Section: MISCELLANEOUS
Examples: user type-in form evaluated :pc 5 (ACL2::PC '5) :pcs app rev (ACL2::PCS 'app 'rev) :length (1 2 3) (ACL2::LENGTH '(1 2 3))
When a keyword, :key, is read as a command, ACL2 determines whether
the symbol with the same name in the "ACL2" package, acl2::key, is
a function or simple macro of n arguments. If so, ACL2 reads n more
objects, obj1, ..., objn, and then acts as though it had read the
following form (for a given key):
(ACL2::key 'obj1 ... 'objn)Thus, by using the keyword command hack you avoid typing the parentheses, the
"ACL2" package name, and the quotation marks.
Note the generality of this hack. Almost any function or macro in
the "ACL2" package can be so invoked, not just ``commands.''
Indeed, there is no such thing as a distinguished class of commands.
The one caveat is that the keyword hack can be used to invoke a
macro only if that macro has a simple argument list -- one
containing no lambda keywords (such as &rest), since they complicate
or render impossible the task of deciding how many objects to read.
Users may take advantage of the keyword command hack by defining
functions and macros in the "ACL2" package.
