		Search-engine friendly clone of the ACL2 documentation.

Support

Keyword-legality

Check whether x is a legal keyword

Returns :single if x is allowed to occur once in the argument list, :multiple if it is allowed to occur more than once, and NIL if not allowed.

Definitions and Theorems

Function: keyword-legality

(defun keyword-legality (x legals)
  (declare (xargs :guard (and (symbolp x)
                              (legal-kwds-p legals))))
  (cond ((atom legals) nil)
        ((eq x (car legals)) :single)
        ((and (consp (car legals))
              (eq x (caar legals)))
         :multiple)
        (t (keyword-legality x (cdr legals)))))