Check if an optional token is a unary operator.
(token-unary-operator-p token?) → yes/no
By this we mean a unary operator according to the grammar, not our abstract syntax, which has a broader notion of unary operator.
Function:
(defun token-unary-operator-p (token?) (declare (xargs :guard (token-optionp token?))) (let ((__function__ 'token-unary-operator-p)) (declare (ignorable __function__)) (or (token-punctuatorp token? "&") (token-punctuatorp token? "*") (token-punctuatorp token? "+") (token-punctuatorp token? "-") (token-punctuatorp token? "~") (token-punctuatorp token? "!"))))
Theorem:
(defthm booleanp-of-token-unary-operator-p (b* ((yes/no (token-unary-operator-p token?))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm non-nil-when-token-unary-operator-p (implies (token-unary-operator-p token?) token?) :rule-classes :compound-recognizer)