		Search-engine friendly clone of the ACL2 documentation.

Support

Legal-kwds-p

List of legal keywords for extract-keywords.

Recognizes a list where each element is either a symbol a singleton list containing a symbol. In extract-keywords, a bare symbol is a legal keyword and a symbol in a singleton list is a keyword that can occur multiple times in an argument list.

Definitions and Theorems

Function: legal-kwds-p

(defun legal-kwds-p (x)
  (declare (xargs :guard t))
  (if (atom x)
      (eq x nil)
    (and (or (symbolp (car x))
             (and (consp (car x))
                  (symbolp (caar x))
                  (not (cdar x))))
         (legal-kwds-p (cdr x)))))