KEYWORD-COMMANDS

how keyword commands are processed
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))
:quit                        (ACL2::QUIT) ; Note: avoid optional argument

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.

See ld-keyword-aliases for how to customize this behavior.

Note the generality of this hack. 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 when the keyword hack is used to invoke a macro, only the required arguments for that macro are read: none of the &optional, &rest, &body, or &key arguments are read, hence they will take on their default values. Users may take advantage of the keyword command hack by defining functions and macros in the "ACL2" package.