Recognize canonical hints specifiers,i.e. hints specifiers that are keyword-value-lists that associated applicability conditions with hints.
(canonical-hints-specifier-p x legal-kwds) → yes/no
These are the hints specifiers that are not abbreviations. See hints-specifier-p and canonicalize-hints-specifier.
Function:
(defun canonical-hints-specifier-p (x legal-kwds) (declare (xargs :guard (keyword-listp legal-kwds))) (let ((__function__ 'canonical-hints-specifier-p)) (declare (ignorable __function__)) (and (keyword-value-listp x) (no-duplicatesp-eq (evens x)) (subsetp-eq (evens x) legal-kwds))))
Theorem:
(defthm booleanp-of-canonical-hints-specifier-p (b* ((yes/no (canonical-hints-specifier-p x legal-kwds))) (booleanp yes/no)) :rule-classes :rewrite)