Check if an optional token may start a specifier or qualifier.
(token-specifier/qualifier-start-p token?) → yes/no
We have predicates to recognize
the starts of type specifiers and qualifiers;
alignment specifiers always start with
There is an overlap between the starts of type specifiers and qualifiers,
namely the
We also include
Function:
(defun token-specifier/qualifier-start-p (token?) (declare (xargs :guard (token-optionp token?))) (let ((__function__ 'token-specifier/qualifier-start-p)) (declare (ignorable __function__)) (or (token-type-specifier-start-p token?) (token-type-qualifier-p token?) (token-keywordp token? "_Alignas") (token-keywordp token? "__attribute") (token-keywordp token? "__attribute__"))))
Theorem:
(defthm booleanp-of-token-specifier/qualifier-start-p (b* ((yes/no (token-specifier/qualifier-start-p token?))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm non-nil-when-token-specifier/qualifier-start-p (implies (token-specifier/qualifier-start-p token?) token?) :rule-classes :compound-recognizer)