Map a token that is a type qualifier to the correspoding type qualifier.
(token-to-type-qualifier token) → tyqual
Function:
(defun token-to-type-qualifier (token) (declare (xargs :guard (tokenp token))) (declare (xargs :guard (token-type-qualifier-p token))) (let ((__function__ 'token-to-type-qualifier)) (declare (ignorable __function__)) (cond ((token-keywordp token "const") (type-qual-const)) ((token-keywordp token "restrict") (type-qual-restrict)) ((token-keywordp token "volatile") (type-qual-volatile)) ((token-keywordp token "_Atomic") (type-qual-atomic)) ((token-keywordp token "__restrict") (type-qual-__restrict)) ((token-keywordp token "__restrict__") (type-qual-__restrict__)) (t (prog2$ (impossible) (irr-type-qual))))))
Theorem:
(defthm type-qualp-of-token-to-type-qualifier (b* ((tyqual (token-to-type-qualifier token))) (type-qualp tyqual)) :rule-classes :rewrite)