Check if an optional token is a type specifier that consists of a single keyword.
(token-type-specifier-keyword-p token?) → yes/no
There are a number of type specifiers that consist of single keywords.
Function:
(defun token-type-specifier-keyword-p (token?) (declare (xargs :guard (token-optionp token?))) (let ((__function__ 'token-type-specifier-keyword-p)) (declare (ignorable __function__)) (or (equal token? (token-keyword "void")) (equal token? (token-keyword "char")) (equal token? (token-keyword "short")) (equal token? (token-keyword "int")) (equal token? (token-keyword "long")) (equal token? (token-keyword "float")) (equal token? (token-keyword "double")) (equal token? (token-keyword "signed")) (equal token? (token-keyword "unsigned")) (equal token? (token-keyword "_Bool")) (equal token? (token-keyword "_Complex")))))
Theorem:
(defthm booleanp-of-token-type-specifier-keyword-p (b* ((yes/no (token-type-specifier-keyword-p token?))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm non-nil-when-token-type-specifier-keyword-p (implies (token-type-specifier-keyword-p token?) token?) :rule-classes :compound-recognizer)