		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))))))