Map a token that is a relational operator to the corresponding relational operator.
Function:
(defun token-to-relational-operator (token) (declare (xargs :guard (tokenp token))) (declare (xargs :guard (token-relational-operator-p token))) (let ((__function__ 'token-to-relational-operator)) (declare (ignorable __function__)) (cond ((equal token (token-punctuator "<")) (binop-lt)) ((equal token (token-punctuator ">")) (binop-gt)) ((equal token (token-punctuator "<=")) (binop-le)) ((equal token (token-punctuator ">=")) (binop-ge)) (t (prog2$ (impossible) (irr-binop))))))
Theorem:
(defthm binopp-of-token-to-relational-operator (b* ((op (token-to-relational-operator token))) (binopp op)) :rule-classes :rewrite)