		Search-engine friendly clone of the ACL2 documentation.

Defsection

Extract-keyword-from-args

Get the value for a keyword argument like :foo value.

(extract-keyword-from-args kwd args) is given kwd, which should be a keyword symbol, and a list of args which are typically the &rest args given to a macro. It scans the list of args, looking for the indicated keyword, and returns (kwd . value), or nil if no such keyword is found. For instance,

(extract-keyword-from-args :bar '(:foo 3 :bar 5 :baz 7))
  -->
(:bar . 5)

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

Function: extract-keyword-from-args

(defun extract-keyword-from-args (kwd args)
  (declare (xargs :guard (keywordp kwd)))
  (cond ((atom args) nil)
        ((eq (car args) kwd)
         (if (consp (cdr args))
             (cons (car args) (cadr args))
           (er hard? 'extract-keyword-from-args
               "Expected something to follow ~s0."
               kwd)))
        (t (extract-keyword-from-args kwd (cdr args)))))