Map a token that is a preincrement or predecrement operator to the corresponding preincrement or predecrement operator.
Function:
(defun token-to-preinc/predec-operator (token) (declare (xargs :guard (tokenp token))) (declare (xargs :guard (token-preinc/predec-operator-p token))) (let ((__function__ 'token-to-preinc/predec-operator)) (declare (ignorable __function__)) (cond ((token-punctuatorp token "++") (unop-preinc)) ((token-punctuatorp token "--") (unop-predec)) (t (prog2$ (impossible) (irr-unop))))))
Theorem:
(defthm unopp-of-token-to-preinc/predec-operator (b* ((op (token-to-preinc/predec-operator token))) (unopp op)) :rule-classes :rewrite)