		Search-engine friendly clone of the ACL2 documentation.

Hints-specifier

Hints-specifier-p

Recognize hints specifiers.

Signature
(hints-specifier-p x legal-kwds) → yes/no
Arguments: legal-kwds — Guard (keyword-listp legal-kwds).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: hints-specifier-p

(defun hints-specifier-p (x legal-kwds)
  (declare (xargs :guard (keyword-listp legal-kwds)))
  (let ((__function__ 'hints-specifier-p))
    (declare (ignorable __function__))
    (or (canonical-hints-specifier-p x legal-kwds)
        (and (true-listp x)
             (not (acl2::first-keyword x))))))

Theorem: booleanp-of-hints-specifier-p

(defthm booleanp-of-hints-specifier-p
  (b* ((yes/no (hints-specifier-p x legal-kwds)))
    (booleanp yes/no))
  :rule-classes :rewrite)