MACRO-ARGS

the formals list of a macro definition 
Major Section:  MISCELLANEOUS


Examples:
(x y z)
(x y z &optional max (base '10 basep))
(x y &rest rst)
(x y &key max base)
(&whole sexpr x y)

The ``lambda-list'' of a macro definition may include simple formal parameter names as well as appropriate uses of the following lambda-list keywords from CLTL (pp. 60 and 145), respecting the order shown: 

  &whole,
  &optional,
  &rest,
  &body,
  &key, and
  &allow-other-keys.
ACL2 does not support &aux and &environment. In addition, we make the following restrictions:

(1) initialization forms in &optional and &key specifiers must be quoted values;

(2) &allow-other-keys may only be used once, as the last specifier; and

(3) destructuring is not allowed.

You are encouraged to experiment with the macro facility. One way to do so is to define a macro that does nothing but return the quotation of its arguments, e.g., 
(defmacro demo (x y &optional opt &key key1 key2)
  (list 'quote (list x y opt key1 key2)))
You may then execute the macro on some sample forms, e.g., 
  term                         value
(demo 1 2)                (1 2 NIL NIL NIL)
(demo 1 2 3)              (1 2 3 NIL NIL)
(demo 1 2 :key1 3)        error:  non-even key/value arglist
                          (because :key1 is used as opt)
(demo 1 2 3 :key2 5)      (1 2 3 NIL 5)
In particular, Common Lisp specifies that if you use both &rest and &key, then both will be bound using the same list of arguments. The following example should serve to illustrate how this works. 
ACL2 !>(defmacro foo (&rest args &key k1 k2 k3)
         (list 'quote (list args k1 k2 k3)))


Summary
Form:  ( DEFMACRO FOO ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 FOO
ACL2 !>(foo :k1 3 :k2 4 :k3 5)
((:K1 3 :K2 4 :K3 5) 3 4 5)
ACL2 !>(foo :k1 3 :k2 4)
((:K1 3 :K2 4) 3 4 NIL)
ACL2 !>

Also see trans.