Check if an optional token is an assignment operator.
(token-assignment-operator-p token?) → yes/no
Function:
(defun token-assignment-operator-p (token?) (declare (xargs :guard (token-optionp token?))) (let ((__function__ 'token-assignment-operator-p)) (declare (ignorable __function__)) (or (equal token? (token-punctuator "=")) (equal token? (token-punctuator "*=")) (equal token? (token-punctuator "/=")) (equal token? (token-punctuator "%=")) (equal token? (token-punctuator "+=")) (equal token? (token-punctuator "-=")) (equal token? (token-punctuator "<<=")) (equal token? (token-punctuator ">>=")) (equal token? (token-punctuator "&=")) (equal token? (token-punctuator "^=")) (equal token? (token-punctuator "|=")))))
Theorem:
(defthm booleanp-of-token-assignment-operator-p (b* ((yes/no (token-assignment-operator-p token?))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm non-nil-when-token-assignment-operator-p (implies (token-assignment-operator-p token?) token?) :rule-classes :compound-recognizer)