		Search-engine friendly clone of the ACL2 documentation.

Defsection

Throw-away-keyword-parts

Throw away any keyword arguments and their values from a macro argument list.

(throw-away-keyword-parts args) is given a list of arguments that are typically the &rest args given to a macro. It scans the arguments for any keyword symbols such as :foo, and throws away both the keyword and the argument that follows it. For instance,

(throw-away-keyword-parts '(x y z :foo 3 :bar 5 blah blah blah))
  -->
'(x y z blah blah blah)

This function is mainly useful for writing macros that mix &rest parts with keyword arguments. See also extract-keyword-from-args.

Function: throw-away-keyword-parts

(defun throw-away-keyword-parts (args)
  (declare (xargs :guard t))
  (cond ((atom args) nil)
        ((keywordp (car args))
         (throw-away-keyword-parts
              (if (consp (cdr args))
                  (cddr args)
                (er hard? 'throw-away-keyword-parts
                    "Expected something to follow ~s0."
                    (car args)))))
        (t (cons (car args)
                 (throw-away-keyword-parts (cdr args))))))