Check if an optional token is a type qualifier.
(token-type-qualifier-p token?) → yes/no
All type qualifiers consist of single keywords.
We also compare the token against the GCC variants
We do the same for the
Function:
(defun token-type-qualifier-p (token?) (declare (xargs :guard (token-optionp token?))) (let ((__function__ 'token-type-qualifier-p)) (declare (ignorable __function__)) (or (token-keywordp token? "const") (token-keywordp token? "restrict") (token-keywordp token? "__restrict") (token-keywordp token? "__restrict__") (token-keywordp token? "volatile") (token-keywordp token? "__volatile") (token-keywordp token? "__volatile__") (token-keywordp token? "_Atomic"))))
Theorem:
(defthm booleanp-of-token-type-qualifier-p (b* ((yes/no (token-type-qualifier-p token?))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm non-nil-when-token-type-qualifier-p (implies (token-type-qualifier-p token?) token?) :rule-classes :compound-recognizer)